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

Theorem exbii 1569
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
exbii  |-  ( E. x ph  <->  E. x ps )

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1568 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1535 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528
This theorem is referenced by:  2exbii  1570  3exbii  1571  exanali  1572  exancom  1573  19.43  1592  excom13  1817  exrot4  1819  eeor  1826  19.12vv  1839  19.41vv  1843  19.41vvv  1844  19.41vvvv  1845  exdistr  1847  19.42vvv  1849  exdistr2  1850  3exdistr  1851  4exdistr  1852  eean  1853  eeeanv  1855  ee4anv  1856  equsex  1902  2sb5  2051  2sb5rf  2056  sbel2x  2064  exsbOLD  2070  2exsb  2071  sb8eu  2161  eu1  2164  eu2  2168  sbmo  2173  moanim  2199  2moswap  2218  2eu1  2223  exists1  2232  clelab  2403  clabel  2404  sbabel  2445  rexbii2  2572  r2exf  2579  r19.41  2692  isset  2792  rexv  2802  ceqsex2  2824  ceqsex3v  2826  gencbvex  2830  vtocl2  2839  vtocl3  2840  spc3gv  2873  ceqsrexv  2901  rexab  2928  rexrab2  2933  euxfr  2951  euind  2952  reu6  2954  reu3  2955  2reuswap  2967  reuind  2968  2reu5lem3  2972  2reu5  2973  sbccomlem  3061  rmo2  3076  rexun  3355  reupick3  3453  abn0  3473  pssnel  3519  rexsns  3671  snprc  3695  euabsn2  3698  reusn  3700  eusn  3703  elunirab  3840  unipr  3841  uniun  3846  uniin  3847  uni0b  3852  uniintsn  3899  iuncom4  3912  dfiun2g  3935  iunn0  3962  iunxiun  3984  disjor  4007  cbvopab2  4090  cbvopab2v  4093  unopab  4095  axrep1  4132  axrep4  4135  axrep5  4136  zfrep4  4139  axsep  4140  zfnuleu  4146  axnulALT  4147  0ex  4150  vprc  4152  inex1  4155  inuni  4173  axpweq  4187  zfpow  4189  axpow2  4190  axpow3  4191  pwex  4193  zfpair  4212  zfpair2  4215  eqvinop  4251  copsexg  4252  opabn0  4295  iunopab  4296  dfid3  4310  zfun  4513  uniex2  4515  uniuni  4527  reusv5OLD  4544  elxp2  4707  opeliunxp  4740  xpiundi  4743  xpiundir  4744  elvvv  4749  eliunxp  4823  relop  4834  opelco2g  4851  cnvco  4865  cnvuni  4866  dfdm3  4867  dfrn2  4868  dfrn3  4869  elrng  4871  dfdm4  4872  eldm2g  4875  dmun  4885  dmin  4886  dmiun  4887  dmuni  4888  dmopab  4889  dmi  4893  elrn  4919  rnopab  4924  dmcosseq  4946  dmres  4976  elres  4990  elsnres  4991  dfima2  5014  elima3  5019  imadmrn  5024  imai  5027  args  5041  rniun  5091  ssrnres  5116  dmsnn0  5138  dmsnopg  5144  elxp4  5160  elxp5  5161  cnvresima  5162  mptpreima  5166  dfco2  5172  coundi  5174  coundir  5175  resco  5177  imaco  5178  rnco  5179  coiun  5182  coi1  5188  coass  5191  dffun2  5265  dffun5  5268  imadif  5327  funimaexg  5329  fun11iun  5493  f11o  5506  brprcneu  5518  dffv2  5592  fndmin  5632  fvresex  5762  abrexco  5766  opabex3  5769  imaiun  5771  abexssex  5781  abexex  5782  isomin  5834  dfoprab2  5895  cbvoprab2  5919  oprabrexex2  5963  releldm2  6170  dfopab2  6174  dfoprab3s  6175  exopxfr  6183  fsplit  6223  frxp  6225  brtpos2  6240  oarec  6560  oeeu  6601  domen  6875  mapsnen  6938  xpsnen  6946  xpcomco  6952  xpassen  6956  inf2  7324  zfinf  7340  axinf2  7341  zfinf2  7343  rankuni  7535  scott0  7556  cp  7561  ween  7662  aceq1  7744  aceq0  7745  aceq2  7746  dfac5lem1  7750  dfac5lem2  7751  dfac5lem3  7752  kmlem3  7778  kmlem14  7789  kmlem15  7790  kmlem16  7791  cflem  7872  cf0  7877  cfval2  7886  cfss  7891  cfslb  7892  fin23lem32  7970  axdc2lem  8074  zfac  8086  ac9  8110  ac9s  8120  axpowndlem3  8221  zfcndrep  8236  zfcndun  8237  zfcndpow  8238  zfcndinf  8240  zfcndac  8241  axgroth5  8446  axgroth2  8447  grothpw  8448  axgroth6  8450  axgroth3  8453  axgroth4  8454  grothprim  8456  grothtsk  8457  genpass  8633  ltexprlem1  8660  ltexprlem4  8663  supmul1  9719  supmullem2  9721  2rexuz  10271  nnwos  10286  hashfun  11389  maxprmfct  12792  4sqlem12  13003  vdwmc  13025  imasleval  13443  isacs2  13555  gsumval3eu  15190  lidlnz  15980  isbasis2g  16686  tgval2  16694  ntreq0  16814  lmff  17029  cmpfi  17135  is1stc2  17168  1stcelcls  17187  isfbas2  17530  elfg  17566  alexsubALTlem3  17743  metrest  18070  cmetss  18740  dchrvmasumlema  20649  isgrpo  20863  ismgm  20987  2reuswap2  23137  rexunirn  23140  nmo  23144  disjorf  23356  axextprim  24047  axrepprim  24048  axunprim  24049  axpowprim  24050  axregprim  24051  axinfprim  24052  axacprim  24053  dftr6  24107  coep  24108  coepr  24109  dffr5  24110  dfpo2  24112  cnvco1  24117  cnvco2  24118  eldm3  24119  fundmpss  24122  dfdm5  24132  dfrn5  24133  domep  24149  axextdfeq  24154  19.12b  24158  axextndbi  24161  wfrlem11  24266  tfrALTlem  24276  frrlem5c  24287  nofulllem5  24360  brtxp  24420  brpprod  24425  brsset  24429  dfon3  24432  brtxpsd  24434  elfix  24443  dffix2  24445  dffun10  24453  elfuns  24454  elsingles  24457  snelsingles  24461  dfiota3  24462  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  funpartfun  24481  funpartfv  24483  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  eeeeanv  24944  fates  24955  eqvinopb  24965  islatalg  25183  dfdir2  25291  cbvprodi  25312  apnei  25520  isalg  25721  algi  25727  cnvresimaOLD  26226  neifg  26320  prtlem16  26737  prter2  26749  diophrex  26855  19.36vv  27581  19.37vv  27583  pm11.58  27589  pm11.6  27591  pm13.192  27610  2sbc5g  27616  iotasbc2  27620  rfcnnnub  27707  stoweidlem34  27783  stoweidlem35  27784  stoweidlem60  27809  rmoanim  27957  2rmoswap  27962  onfrALTlem5  28307  onfrALTlem1  28313  a9e2nd  28324  2sb5nd  28326  en3lplem2VD  28620  relopabVD  28677  a9e2ndVD  28684  2sb5ndVD  28686  a9e2ndALT  28707  2sb5ndALT  28709  bnj89  28747  bnj133  28753  bnj1019  28811  bnj1101  28816  bnj1109  28818  bnj1143  28822  bnj1198  28828  bnj1304  28852  bnj605  28939  bnj607  28948  bnj600  28951  bnj865  28955  bnj916  28965  bnj983  28983  bnj985  28985  bnj996  28987  bnj1033  28999  bnj1083  29008  bnj1090  29009  bnj1093  29010  bnj1110  29012  bnj1128  29020  bnj1145  29023  bnj1171  29030  bnj1172  29031  bnj1174  29033  bnj1176  29035  bnj1186  29037  bnj1189  29039  bnj1253  29047  bnj1279  29048  bnj1371  29059  bnj1374  29061  bnj1312  29088  equsexv-x12  29113  equvinv  29114  islshpat  29207  islpln5  29724  islvol5  29768  pmapglb  29959  polval2N  30095  cdlemftr3  30754  dibelval3  31337  dicelval3  31370  dihglb2  31532
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-ex 1529
  Copyright terms: Public domain W3C validator