Theorem dfrex2 2718

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)

Assertion

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

Proof of Theorem dfrex2

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

Syntax hints:   -. wn 3   <-> wb 184   A.wral 2705   E.wrex 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-ral 2710  df-rex 2711

This theorem is referenced by:  nfrexd  2758  nfrex  2761  rexim  2810  r19.30  2855  r19.35  2857  cbvrexf  2932  rspcimedv  3064  sbcrextOLD  3256  sbcrext  3257  cbvrexcsf  3308  r19.9rzv  3762  rexxfrd  4495  rexxfr2d  4497  rexxfr  4500  rexiunxp  4967  rexxpf  4974  rexrnmpt  5841  cbvexfo  5981  rexrnmpt2  6195  tz7.49  6886  abianfp  6900  dfsup2  7680  supnub  7700  wofib  7747  zfregs2  7941  alephval3  8268  ac6n  8642  prmreclem5  13964  sylow1lem3  16079  ordtrest2lem  18649  trfil2  19302  alexsubALTlem3  19463  alexsubALTlem4  19464  evth  20373  lhop1lem  21327  nmobndseqi  24002  chpssati  25590  chrelat3  25598  nn0min  25913  xrnarchi  26025  ordtrest2NEWlem  26206  dffr5  27410  fdc  28485  unxpwdom3  29293  rexxfrd2  29984  zfregs2VD  31300  lpssat  32252  lssat  32255  lfl1  32309  atlrelat1  32560