Theorem dfrex2 2996

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

Syntax hints:   -. wn 3   <-> wb 196   A.wral 2912   E.wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexanali  2998  nfrexd  3006  rexim  3008  r19.23v  3023  r19.30  3082  r19.35  3084  cbvrexf  3166  rspcimedv  3311  sbcrext  3511  sbcrextOLD  3512  cbvrexcsf  3566  rabn0  3958  r19.9rzv  4065  rexxfrd  4881  rexxfr2d  4883  rexxfrd2  4885  rexxfr  4888  rexiunxp  5262  rexxpf  5269  rexrnmpt  6369  cbvexfo  6545  rexrnmpt2  6776  tz7.49  7540  dfsup2  8350  supnub  8368  infnlb  8398  wofib  8450  zfregs2  8609  alephval3  8933  ac6n  9307  prmreclem5  15624  sylow1lem3  18015  ordtrest2lem  21007  trfil2  21691  alexsubALTlem3  21853  alexsubALTlem4  21854  evth  22758  lhop1lem  23776  vdn0conngrumgrv2  27056  nmobndseqi  27634  chpssati  29222  chrelat3  29230  nn0min  29567  xrnarchi  29738  ordtrest2NEWlem  29968  dffr5  31643  nosupbnd1lem4  31857  poimirlem1  33410  poimirlem26  33435  poimirlem27  33436  fdc  33541  lpssat  34300  lssat  34303  lfl1  34357  atlrelat1  34608  unxpwdom3  37665  ss2iundf  37951  zfregs2VD  39076