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

Theorem exbii 1814
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1 (𝜑𝜓)
Assertion
Ref Expression
exbii (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1813 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1764 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  2exbii  1815  3exbii  1816  exanali  1826  exancom  1827  19.43  1850  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistr  1922  19.42vvv  1924  exdistr2  1925  3exdistr  1926  sbequ8  1942  19.12vvv  1963  equsexvw  1978  excom13  2084  exrot4  2086  equsexv  2147  eeor  2207  19.12vv  2216  eean  2217  eeeanv  2219  ee4anv  2220  equsexALT  2329  2sb5  2471  2sb5rf  2479  2sb8e  2495  sb8eu  2532  eu1  2539  sbmo  2544  2moswap  2576  exists1  2590  clabel  2778  sbabel  2822  nabbi  2925  rexbii2  3068  r2exlem  3088  r19.41v  3118  r19.41  3119  isset  3238  rexv  3251  ceqsex2  3275  ceqsex3v  3277  gencbvex  3281  vtocl2  3292  vtocl3  3293  spc3gv  3329  ceqsrexv  3367  rexab  3402  rexrab2  3407  euxfr  3425  euind  3426  reu6  3428  reu3  3429  2reuswap  3443  reuind  3444  2reu5lem3  3448  2reu5  3449  sbccomlem  3541  rmo2  3559  rexun  3826  reupick3  3945  euelss  3947  abn0  3987  pssnel  4072  rexsns  4249  exsnrex  4253  snprc  4285  euabsn2  4292  reusn  4294  eusn  4297  elpreqpr  4427  elunirab  4480  unipr  4481  uniun  4488  uniin  4489  uni0b  4495  uniintsn  4546  iuncom4  4560  dfiun2g  4584  iunn0  4612  iunxiun  4640  disjor  4666  cbvopab2  4757  cbvopab2v  4760  unopab  4761  axrep1  4805  axrep4  4808  axrep5  4809  zfrep4  4812  axsep  4813  zfnuleu  4819  axnulALT  4820  0ex  4823  vprc  4829  inex1  4832  inuni  4856  axpweq  4872  zfpow  4874  axpow2  4875  axpow3  4876  pwex  4878  zfpair  4934  zfpair2  4937  eqvinop  4984  copsexg  4985  opabn0  5035  iunopab  5041  dfid3  5054  elxp2OLD  5167  opeliunxp  5204  xpiundi  5207  xpiundir  5208  elvvv  5212  csbxp  5234  eliunxp  5292  exopxfr  5298  relop  5305  opelco2g  5322  cnvco  5340  cnvuni  5341  dfdm3  5342  dfrn2  5343  dfrn3  5344  elrng  5346  dfdm4  5348  csbdm  5350  eldm2g  5352  dmun  5363  dmin  5364  dmiun  5365  dmuni  5366  dmopab  5367  dmi  5372  elrn  5398  rnopab  5402  dmcosseq  5419  dmres  5454  elres  5470  elsnres  5471  dfima2  5503  elima3  5508  imadmrn  5511  imai  5513  args  5528  rniun  5578  xpdifid  5597  ssrnres  5607  dmsnn0  5635  dmsnopg  5642  cnvresima  5661  mptpreima  5666  dfco2  5672  coundi  5674  coundir  5675  resco  5677  imaco  5678  rnco  5679  coiun  5683  coi1  5689  coass  5692  xpco  5713  elsnxp  5715  elsnxpOLD  5716  dffun2  5936  dffun5  5939  imadif  6011  funimaexg  6013  brprcneu  6222  dffv2  6310  fndmin  6364  fvn0ssdmfun  6390  abrexco  6542  imaiun  6543  isomin  6627  dfoprab2  6743  cbvoprab2  6770  zfun  6992  uniex2  6994  uniuni  7013  elxp4  7152  elxp5  7153  fun11iun  7168  f11o  7170  fvresex  7181  opabex3d  7187  opabex3  7188  abexssex  7191  abexex  7193  oprabrexex2  7200  releldm2  7262  dfopab2  7266  dfoprab3s  7267  fsplit  7327  frxp  7332  suppvalbr  7344  cnvimadfsn  7349  brtpos2  7403  wfrfun  7470  dfrecs3  7514  oarec  7687  oeeu  7728  domen  8010  mapsnen  8076  xpsnen  8085  xpcomco  8091  xpassen  8095  inf2  8558  zfinf  8574  axinf2  8575  zfinf2  8577  rankuni  8764  scott0  8787  cp  8792  ween  8896  aceq1  8978  aceq0  8979  aceq2  8980  dfac5lem1  8984  dfac5lem2  8985  dfac5lem3  8986  kmlem3  9012  kmlem14  9023  kmlem15  9024  kmlem16  9025  cflem  9106  cf0  9111  cfval2  9120  cfss  9125  cfslb  9126  fin23lem32  9204  axdc2lem  9308  zfac  9320  ac9  9343  ac9s  9353  axpowndlem3  9459  zfcndrep  9474  zfcndun  9475  zfcndpow  9476  zfcndinf  9478  zfcndac  9479  axgroth5  9684  axgroth2  9685  grothpw  9686  axgroth6  9688  axgroth3  9691  axgroth4  9692  grothprim  9694  grothtsk  9695  genpass  9869  ltexprlem1  9896  ltexprlem4  9899  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  2rexuz  11778  nnwos  11793  hashfun  13262  wwlktovfo  13747  xpcogend  13759  cbvsum  14469  cbvprod  14689  iprodmul  14778  maxprmfct  15468  4sqlem12  15707  vdwmc  15729  cshwrepswhash1  15856  imasleval  16248  isacs2  16361  cicsym  16511  gsumval3eu  18351  lidlnz  19276  isbasis2g  20800  tgval2  20808  ntreq0  20929  lmff  21153  cmpfi  21259  is1stc2  21293  1stcelcls  21312  unisngl  21378  isfbas2  21686  elfg  21722  alexsubALTlem3  21900  ustfilxp  22063  metrest  22376  metuel2  22417  restmetu  22422  cmetss  23159  dchrvmasumlema  25234  istrkg2ld  25404  istrkg3ld  25405  1loopgrvd2  26455  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnextsur  26863  isgrpo  27479  nmo  29453  2reuswap2  29455  rexunirn  29458  disjorf  29518  fcoinvbr  29545  mpt2mptxf  29605  cnvoprabOLD  29626  fpwrelmapffslem  29635  ordtconnlem1  30098  ddemeas  30427  omssubaddlem  30489  omssubadd  30490  eulerpartlemgvv  30566  bnj89  30915  bnj133  30921  bnj1019  30976  bnj1101  30981  bnj1109  30983  bnj1143  30987  bnj1198  30992  bnj1304  31016  bnj605  31103  bnj607  31112  bnj600  31115  bnj865  31119  bnj916  31129  bnj983  31147  bnj985  31149  bnj996  31151  bnj1033  31163  bnj1083  31172  bnj1090  31173  bnj1093  31174  bnj1110  31176  bnj1128  31184  bnj1145  31187  bnj1171  31194  bnj1172  31195  bnj1174  31197  bnj1176  31199  bnj1186  31201  bnj1189  31203  bnj1253  31211  bnj1279  31212  bnj1371  31223  bnj1374  31225  bnj1312  31252  axextprim  31704  axrepprim  31705  axunprim  31706  axpowprim  31707  axregprim  31708  axinfprim  31709  axacprim  31710  dftr6  31766  coep  31767  coepr  31768  dffr5  31769  dfpo2  31771  cnvco1  31775  cnvco2  31776  eldm3  31777  fundmpss  31790  dfdm5  31800  dfrn5  31801  elima4  31803  domep  31822  axextdfeq  31827  19.12b  31831  axextndbi  31834  frrlem5c  31911  brtxp  32112  brpprod  32117  brsset  32121  dfon3  32124  brtxpsd  32126  elfix  32135  dffix2  32137  sscoid  32145  dffun10  32146  elfuns  32147  elsingles  32150  snelsingles  32154  dfiota3  32155  brimg  32169  brapply  32170  brcup  32171  brcap  32172  brsuccf  32173  funpartlem  32174  brrestrict  32181  dfrecs2  32182  dfrdg4  32183  neifg  32491  bj-equsexval  32763  bj-dfssb2  32765  bj-eeanvw  32829  bj-clabel  32908  bj-axrep1  32913  bj-axrep4  32916  bj-axrep5  32917  bj-axsep  32918  bj-zfpow  32920  bj-cleljustab  32972  bj-denotes  32983  bj-rexvwv  32991  bj-rexcom4  32994  bj-csbsnlem  33023  bj-snsetex  33076  bj-elsngl  33081  bj-snglc  33082  bj-nul  33143  bj-restpw  33170  bj-restuni  33175  bj-dfmpt2a  33196  mptsnunlem  33315  topdifinffinlem  33325  poimirlem26  33565  ismblfin  33580  itg2addnclem3  33593  itg2addnc  33594  ismgmOLD  33779  sbcexfi  34050  sbccom2lem  34059  eldmres  34177  ecinn0  34258  ineleq  34259  moantr  34267  rnxrn  34296  rnxrnres  34297  dfcoss2  34311  dfcoss3  34312  1cossres  34324  cocossss  34331  rncossdmcoss  34345  eldmcoss2  34349  coss0  34369  cossid  34370  dfssr2  34389  prtlem16  34473  prter2  34485  islshpat  34622  islpln5  35139  islvol5  35183  pmapglb  35374  polval2N  35510  cdlemftr3  36170  dibelval3  36753  dicelval3  36786  dihglb2  36948  diophrex  37656  rp-isfinite6  38181  relintab  38206  imaiun1  38260  coiun1  38261  ndisj  38380  clsk3nimkb  38655  19.36vv  38899  19.37vv  38901  pm11.58  38907  pm11.6  38909  pm13.192  38928  2sbc5g  38934  iotasbc2  38938  onfrALTlem5  39074  onfrALTlem1  39080  ax6e2nd  39091  2sb5nd  39093  en3lplem2VD  39393  onfrALTlem5VD  39435  relopabVD  39451  ax6e2ndVD  39458  2sb5ndVD  39460  ax6e2ndALT  39480  2sb5ndALT  39482  rfcnnnub  39509  inn0f  39556  stoweidlem34  40569  stoweidlem35  40570  stoweidlem60  40595  smfpimcc  41335  rmoanim  41500  2rmoswap  41505  sprid  42049  opeliun2xp  42436  eliunxp2  42437  setrec1lem3  42761  elpglem3  42784  eximp-surprise  42858
  Copyright terms: Public domain W3C validator