Theorem dfrex2 1659

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 1656	. 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 1648  E.wrex 1649

This theorem is referenced by:  r19.35 1762  sbcrext 1994  sbcrexgf 1996  r19.9rzv 2353  rexpr 2433  rexxfrd 2904  rexxfr 2907  rexxp 3225  cbvexfo 3892  tz7.49 3965  abianfp 3968  supnub 4591  ac6n 4767  alephval3 4914  ssxr 5552  supxrre 6085  infxpidmlem12 7564  lpbl 7877  chpssat 10285  chrelat3t 10293

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain