Theorem dfrex2 2857

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)

Assertion

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

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 2852	. 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 2799   E.wrex 2800

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-ral 2804  df-rex 2805

This theorem is referenced by:  nfrexd  2887  nfrex  2890  rexim  2926  r19.30  2971  r19.35  2973  cbvrexf  3048  rspcimedv  3181  sbcrextOLD  3376  sbcrext  3377  cbvrexcsf  3431  r19.9rzv  3885  rexxfrd  4618  rexxfr2d  4620  rexxfr  4623  rexiunxp  5091  rexxpf  5098  rexrnmpt  5965  cbvexfo  6106  rexrnmpt2  6319  tz7.49  7013  dfsup2  7807  supnub  7827  wofib  7874  zfregs2  8068  alephval3  8395  ac6n  8769  prmreclem5  14103  sylow1lem3  16224  ordtrest2lem  18949  trfil2  19602  alexsubALTlem3  19763  alexsubALTlem4  19764  evth  20673  lhop1lem  21628  nmobndseqi  24358  chpssati  25946  chrelat3  25954  nn0min  26262  xrnarchi  26373  ordtrest2NEWlem  26520  dffr5  27730  fdc  28812  unxpwdom3  29619  rexxfrd2  30309  zfregs2VD  31932  lpssat  33021  lssat  33024  lfl1  33078  atlrelat1  33329