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

Theorem rexnal 2836
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 2835 . 2  |-  ( A. x  e.  A  ph  <->  -.  E. x  e.  A  -.  ph )
21con2bii 334 1  |-  ( E. x  e.  A  -.  ph  <->  -. 
A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188   A.wral 2737   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  dfral2OLD  2837  rexnal2  2891  rexnal3  2892  rexanaliOLD  2895  2ralor  2960  elpwunsn  4012  uni0b  4223  iundif2  4345  weniso  6245  rexrnmpt2  6412  onnseq  7063  ixp0  7555  boxcutc  7565  isfinite2  7829  ordtypelem9  8041  ordtypelem10  8042  unbndrank  8313  tcrank  8355  infxpenlem  8444  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  12204  hashfun  12609  hashge2el2dif  12637  limsuplt  13538  limsupltOLD  13539  fprodle  14050  alzdvds  14355  isprm5  14651  ncoprmlnprm  14677  pc2dvds  14828  vdwnn  14948  ramcl  14987  cshwshashlem1  15066  cshwshash  15075  isnsgrp  16531  isnmnd  16540  lt6abl  17529  mdetunilem8  19644  fctop  20019  cctop  20021  t0dist  20341  ist0-3  20361  pthaus  20653  txkgen  20667  xkohaus  20668  fbfinnfr  20856  isufil2  20923  hausflim  20996  fclscf  21040  bcth  22297  minveclem3b  22370  minveclem3bOLD  22382  pmltpc  22401  volsup  22509  volsup2  22563  itg2seq  22700  itg2cn  22721  tdeglem4  23009  aaliou3lem9  23306  ftalem7  24005  dchrptlem3  24194  dchrsum2  24196  tglowdim1i  24545  tgdim01  24551  tglowdim2ln  24696  brbtwn2  24935  colinearalg  24940  axlowdimlem6  24977  axlowdimlem14  24985  usgra2edg1  25110  frgra2v  25727  4cycl2vnunb  25745  vdn0frgrav2  25751  vdgn0frgrav2  25752  nmounbi  26417  nmobndseqi  26420  minvecolem5  26523  minvecolem5OLD  26533  xrnarchi  28501  isarchi2  28502  ordtconlem1  28730  lmdvg  28759  hasheuni  28906  voliune  29052  volfiniune  29053  ballotlemodife  29330  ballotlem4  29331  bnj1542  29668  bnj110  29669  bnj1189  29818  noseponlem  30555  nodenselem4  30573  nodenselem5  30574  nofulllem5  30595  dfrecs2  30717  brub  30721  filnetlem4  31037  relowlpssretop  31767  poimirlem23  31963  poimirlem30  31970  poimirlem32  31972  poimir  31973  mblfinlem1  31977  fphpd  35659  fiphp3d  35662  rencldnfilem  35663  pellfundglb  35733  ndisj2  37389  infrpge  37574  limcrecl  37709  stoweidlem14  37874  stoweidlem34  37895  salexct  38193  n0snor2el  38996  usgr2edg1  39292  usg2edgneu  39777  copisnmnd  39862  zrninitoringc  40126  pgrpgt2nabl  40204  islindeps  40299  islininds2  40330  ldepslinc  40355
  Copyright terms: Public domain W3C validator