Theorem dfrex2 1656

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 1653	. 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 1645  E.wrex 1646

This theorem is referenced by:  r19.35 1759  sbcrext 1991  sbcrexgf 1993  r19.9rzv 2349  rexpr 2429  rexxfrd 2898  rexxfr 2901  rexxp 3219  cbvexfo 3886  tz7.49 3959  abianfp 3962  supnub 4582  ac6n 4757  alephval3 4903  ssxr 5540  supxrre 6083  infxpidmlem12 7563  lpbl 7880  chpssat 10290  chrelat3t 10298

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-ral 1649  df-rex 1650

Copyright terms: Public domain