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

Theorem rexnal 2873
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 9-Dec-2019.)
Assertion
Ref Expression
rexnal  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )

Proof of Theorem rexnal
StepHypRef Expression
1 dfral2 2872 . 2  |-  ( A. x  e.  A  ph  <->  -.  E. x  e.  A  -.  ph )
21con2bii 333 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187   A.wral 2775   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2780  df-rex 2781
This theorem is referenced by:  dfral2OLD  2875  rexnal2  2929  rexnal3  2930  rexanaliOLD  2933  2ralor  2998  elpwunsn  4037  uni0b  4241  iundif2  4363  weniso  6256  rexrnmpt2  6422  onnseq  7067  ixp0  7559  boxcutc  7569  isfinite2  7831  ordtypelem9  8043  ordtypelem10  8044  unbndrank  8314  tcrank  8356  infxpenlem  8445  kmlem3  8582  kmlem7  8586  kmlem8  8587  kmlem13  8592  cfeq0  8686  isf32lem2  8784  isf32lem5  8787  isf34lem4  8807  fin1a2lem7  8836  ac6n  8915  alephval2  8997  pwfseqlem3  9085  inttsk  9199  nqereu  9354  npomex  9421  prlem934  9458  arch  10866  qextlt  11496  qextle  11497  xralrple  11498  xrsupsslem  11592  xrinfmsslem  11593  supxrbnd1  11607  supxrbnd2  11608  supxrbnd  11614  fsuppmapnn0fiubex  12203  hashfun  12606  hashge2el2dif  12633  limsuplt  13523  limsupltOLD  13524  fprodle  14035  alzdvds  14340  isprm5  14636  ncoprmlnprm  14662  pc2dvds  14813  vdwnn  14933  ramcl  14972  cshwshashlem1  15051  cshwshash  15060  isnsgrp  16516  isnmnd  16525  lt6abl  17514  mdetunilem8  19628  fctop  20003  cctop  20005  t0dist  20325  ist0-3  20345  pthaus  20637  txkgen  20651  xkohaus  20652  fbfinnfr  20840  isufil2  20907  hausflim  20980  fclscf  21024  bcth  22281  minveclem3b  22354  minveclem3bOLD  22366  pmltpc  22385  volsup  22493  volsup2  22547  itg2seq  22684  itg2cn  22705  tdeglem4  22993  aaliou3lem9  23290  ftalem7  23989  dchrptlem3  24178  dchrsum2  24180  tglowdim1i  24529  tgdim01  24535  tglowdim2ln  24680  brbtwn2  24919  colinearalg  24924  axlowdimlem6  24961  axlowdimlem14  24969  usgra2edg1  25094  frgra2v  25710  4cycl2vnunb  25728  vdn0frgrav2  25734  vdgn0frgrav2  25735  nmounbi  26400  nmobndseqi  26403  minvecolem5  26506  minvecolem5OLD  26516  xrnarchi  28493  isarchi2  28494  ordtconlem1  28723  lmdvg  28752  hasheuni  28899  voliune  29045  volfiniune  29046  ballotlemodife  29323  ballotlem4  29324  bnj1542  29661  bnj110  29662  bnj1189  29811  nodenselem4  30563  nodenselem5  30564  nofulllem5  30585  dfrecs2  30707  brub  30711  filnetlem4  31027  relowlpssretop  31705  poimirlem23  31874  poimirlem30  31881  poimirlem32  31883  poimir  31884  mblfinlem1  31888  fphpd  35575  fiphp3d  35578  rencldnfilem  35579  pellfundglb  35650  ndisj2  37248  infrpge  37413  limcrecl  37526  stoweidlem14  37691  stoweidlem34  37712  n0snor2el  38698  usg2edgneu  38910  copisnmnd  38995  zrninitoringc  39259  pgrpgt2nabl  39339  islindeps  39434  islininds2  39465  ldepslinc  39490
  Copyright terms: Public domain W3C validator