Theorem dfrex2 2876

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 2871	. 2 |- ( A. x e. A -. ph <-> -. E. x e. A ph )
2	1	con2bii 333	1 |- ( E. x e. A ph <-> -. A. x e. A -. ph )

Syntax hints:   -. wn 3   <-> wb 187   A.wral 2775   E.wrex 2776

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

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781

This theorem is referenced by:  rexanali  2878  nfrexd  2887  nfrexOLD  2889  rexim  2890  r19.23v  2905  r19.30  2973  r19.35  2975  cbvrexf  3050  rspcimedv  3184  sbcrext  3373  cbvrexcsf  3428  r19.9rzv  3891  rexxfrd  4632  rexxfr2d  4634  rexxfr  4637  rexiunxp  4990  rexxpf  4997  rexrnmpt  6043  cbvexfo  6199  rexrnmpt2  6422  tz7.49  7166  dfsup2  7960  supnub  7978  infnlb  8010  wofib  8062  zfregs2  8218  alephval3  8541  ac6n  8915  prmreclem5  14851  sylow1lem3  17239  ordtrest2lem  20205  trfil2  20888  alexsubALTlem3  21050  alexsubALTlem4  21051  evth  21973  lhop1lem  22951  nmobndseqi  26405  chpssati  28001  chrelat3  28009  nn0min  28378  xrnarchi  28495  ordtrest2NEWlem  28723  dffr5  30387  poimirlem1  31854  poimirlem26  31879  poimirlem27  31880  fdc  31987  lpssat  32497  lssat  32500  lfl1  32554  atlrelat1  32805  unxpwdom3  35872  ss2iundf  36110  zfregs2VD  37097  rexxfrd2  38709