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

Theorem dfrex2 2556
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 2553 . 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 2543   E.wrex 2544
This theorem is referenced by:  nfrexd  2595  nfrex  2598  rexim  2647  r19.30  2685  r19.35  2687  cbvrexf  2759  rspcimedv  2886  sbcrext  3064  cbvrexcsf  3144  r19.9rzv  3548  rexxfrd  4549  rexxfr2d  4551  rexxfr  4554  rexiunxp  4826  rexxpf  4831  rexrnmpt  5670  cbvexfo  5800  rexrnmpt2  5959  tz7.49  6457  abianfp  6471  dfsup2  7195  supnub  7213  wofib  7260  zfregs2  7415  alephval3  7737  ac6n  8112  prmreclem5  12967  sylow1lem3  14911  ordtrest2lem  16933  trfil2  17582  alexsubALTlem3  17743  alexsubALTlem4  17744  evth  18457  lhop1lem  19360  nmobndseqi  21357  chpssati  22943  chrelat3  22951  dffr5  24110  fdc  26455  unxpwdom3  27256  zfregs2VD  28617  lpssat  29203  lssat  29206  lfl1  29260  atlrelat1  29511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator