Theorem dfrex2 2837

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

Syntax hints:   -. wn 3   <-> wb 188   A.wral 2736   E.wrex 2737

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

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-ral 2741  df-rex 2742

This theorem is referenced by:  rexanali  2839  nfrexd  2848  nfrexOLD  2850  rexim  2851  r19.23v  2866  r19.30  2934  r19.35  2936  cbvrexf  3013  rspcimedv  3151  sbcrext  3340  cbvrexcsf  3395  r19.9rzv  3862  rexxfrd  4614  rexxfr2d  4616  rexxfr  4619  rexiunxp  4974  rexxpf  4981  rexrnmpt  6030  cbvexfo  6186  rexrnmpt2  6409  tz7.49  7159  dfsup2  7955  supnub  7973  infnlb  8005  wofib  8057  zfregs2  8214  alephval3  8538  ac6n  8912  prmreclem5  14857  sylow1lem3  17245  ordtrest2lem  20212  trfil2  20895  alexsubALTlem3  21057  alexsubALTlem4  21058  evth  21980  lhop1lem  22958  nmobndseqi  26413  chpssati  28009  chrelat3  28017  nn0min  28377  xrnarchi  28494  ordtrest2NEWlem  28721  dffr5  30386  poimirlem1  31934  poimirlem26  31959  poimirlem27  31960  fdc  32067  lpssat  32573  lssat  32576  lfl1  32630  atlrelat1  32881  unxpwdom3  35947  ss2iundf  36245  zfregs2VD  37231  rexxfrd2  39003