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

Theorem dfrex2 2569
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
dfrex2  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )

Proof of Theorem dfrex2
StepHypRef Expression
1 ralnex 2566 . 2  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
21con2bii 322 1  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wral 2556   E.wrex 2557
This theorem is referenced by:  nfrexd  2608  nfrex  2611  rexim  2660  r19.30  2698  r19.35  2700  cbvrexf  2772  rspcimedv  2899  sbcrext  3077  cbvrexcsf  3157  r19.9rzv  3561  rexxfrd  4565  rexxfr2d  4567  rexxfr  4570  rexiunxp  4842  rexxpf  4847  rexrnmpt  5686  cbvexfo  5816  rexrnmpt2  5975  tz7.49  6473  abianfp  6487  dfsup2  7211  supnub  7229  wofib  7276  zfregs2  7431  alephval3  7753  ac6n  8128  prmreclem5  12983  sylow1lem3  14927  ordtrest2lem  16949  trfil2  17598  alexsubALTlem3  17759  alexsubALTlem4  17760  evth  18473  lhop1lem  19376  nmobndseqi  21373  chpssati  22959  chrelat3  22967  dffr5  24181  fdc  26558  unxpwdom3  27359  zfregs2VD  28933  lpssat  29825  lssat  29828  lfl1  29882  atlrelat1  30133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator