Theorem dfrex2 1663

Description: Relationship between restricted universal and existential quantifiers.

Assertion

Ref	Expression
dfrex2	|- (E.x e. A ph <-> -. A.x e. A -. ph)

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 1660	. 2 |- (A.x e. A -. ph <-> -. E.x e. A ph)
2	1	con2bii 221	1 |- (E.x e. A ph <-> -. A.x e. A -. ph)

Syntax hints:  -. wn 2   <-> wb 146  A.wral 1652  E.wrex 1653

This theorem is referenced by:  r19.35 1766  sbcrext 2001  sbcrexgf 2003  r19.9rzv 2361  rexpr 2441  rexxfrd 2914  rexxfr 2917  rexxp 3235  cbvexfo 3902  tz7.49 3975  abianfp 3978  supnub 4597  ac6n 4774  alephval3 4923  ssxr 5560  supxrre 6115  infxpidmlem12 7596  lpbl 7906  chpssati 10315  chrelat3 10323

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 967  ax-4 977  ax-5o 979

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-ral 1656  df-rex 1657

Copyright terms: Public domain