Theorem dfrex2 2918

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 2913	. 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 2817   E.wrex 2818

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2822  df-rex 2823

This theorem is referenced by:  rexanali  2920  nfrexd  2929  nfrexOLD  2931  rexim  2932  r19.23v  2947  r19.30  3011  r19.35  3013  cbvrexf  3088  rspcimedv  3221  sbcrextOLD  3418  sbcrext  3419  cbvrexcsf  3473  r19.9rzv  3928  rexxfrd  4668  rexxfr2d  4670  rexxfr  4673  rexiunxp  5149  rexxpf  5156  rexrnmpt  6042  cbvexfo  6192  rexrnmpt2  6413  tz7.49  7122  dfsup2  7914  supnub  7934  wofib  7982  zfregs2  8176  alephval3  8503  ac6n  8877  prmreclem5  14314  sylow1lem3  16493  ordtrest2lem  19572  trfil2  20256  alexsubALTlem3  20417  alexsubALTlem4  20418  evth  21327  lhop1lem  22282  nmobndseqi  25517  chpssati  27105  chrelat3  27113  nn0min  27435  xrnarchi  27552  ordtrest2NEWlem  27729  dffr5  29109  fdc  30165  unxpwdom3  30969  rexxfrd2  32094  zfregs2VD  33122  lpssat  34211  lssat  34214  lfl1  34268  atlrelat1  34519