MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfrex2 Structured version   Unicode version

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
StepHypRef Expression
1 ralnex 2852 . 2  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
21con2bii 332 1  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator