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

Theorem dfrex2 2710
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 2707 . 2  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
21con2bii 323 1  |-  ( E. x  e.  A  ph  <->  -. 
A. x  e.  A  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wral 2697   E.wrex 2698
This theorem is referenced by:  nfrexd  2750  nfrex  2753  rexim  2802  r19.30  2845  r19.35  2847  cbvrexf  2919  rspcimedv  3046  sbcrext  3226  cbvrexcsf  3304  r19.9rzv  3714  rexxfrd  4730  rexxfr2d  4732  rexxfr  4735  rexiunxp  5007  rexxpf  5012  rexrnmpt  5871  cbvexfo  6015  rexrnmpt2  6177  tz7.49  6694  abianfp  6708  dfsup2  7439  supnub  7457  wofib  7504  zfregs2  7659  alephval3  7981  ac6n  8355  prmreclem5  13278  sylow1lem3  15224  ordtrest2lem  17257  trfil2  17909  alexsubALTlem3  18070  alexsubALTlem4  18071  evth  18974  lhop1lem  19887  nmobndseqi  22270  chpssati  23856  chrelat3  23864  xrnarchi  24244  dffr5  25366  fdc  26403  unxpwdom3  27188  rexxfrd2  28024  zfregs2VD  28854  lpssat  29712  lssat  29715  lfl1  29769  atlrelat1  30020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator