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

Theorem exbii 1771
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 1770 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1721 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  2exbii  1772  3exbii  1773  exanali  1783  exancom  1784  19.43  1807  sbequ8  1882  19.12vvv  1904  19.41vv  1912  19.41vvv  1913  19.41vvvv  1914  exdistr  1916  19.42vvv  1918  exdistr2  1919  3exdistr  1920  equsexvw  1929  excom13  2041  exrot4  2043  equsexv  2106  eeor  2168  19.12vv  2179  eean  2180  eeeanv  2182  ee4anv  2183  equsexALT  2293  2sb5  2442  2sb5rf  2450  2sb8e  2466  sb8eu  2502  eu1  2509  sbmo  2514  2moswap  2546  exists1  2560  clabel  2746  sbabel  2789  nabbi  2892  rexbii2  3034  r2exlem  3054  r19.41v  3083  r19.41  3084  isset  3197  rexv  3210  ceqsex2  3234  ceqsex3v  3236  gencbvex  3240  vtocl2  3251  vtocl3  3252  spc3gv  3288  ceqsrexv  3324  rexab  3356  rexrab2  3361  euxfr  3379  euind  3380  reu6  3382  reu3  3383  2reuswap  3397  reuind  3398  2reu5lem3  3402  2reu5  3403  sbccomlem  3495  rmo2  3512  rexun  3777  reupick3  3894  euelss  3896  abn0  3934  pssnel  4017  rexsns  4195  exsnrex  4199  snprc  4230  euabsn2  4237  reusn  4239  eusn  4242  elpreqpr  4371  elunirab  4421  unipr  4422  uniun  4429  uniin  4430  uni0b  4436  uniintsn  4486  iuncom4  4501  dfiun2g  4525  iunn0  4553  iunxiun  4581  disjor  4607  cbvopab2  4696  cbvopab2v  4699  unopab  4700  axrep1  4742  axrep4  4745  axrep5  4746  zfrep4  4749  axsep  4750  zfnuleu  4756  axnulALT  4757  0ex  4760  vprc  4766  inex1  4769  inuni  4796  axpweq  4812  zfpow  4814  axpow2  4815  axpow3  4816  pwex  4818  zfpair  4875  zfpair2  4878  eqvinop  4925  copsexg  4926  opabn0  4976  iunopab  4982  dfid3  5000  elxp2OLD  5103  opeliunxp  5141  xpiundi  5144  xpiundir  5145  elvvv  5149  csbxp  5171  eliunxp  5229  exopxfr  5235  relop  5242  opelco2g  5259  cnvco  5278  cnvuni  5279  dfdm3  5280  dfrn2  5281  dfrn3  5282  elrng  5284  dfdm4  5286  csbdm  5288  eldm2g  5290  dmun  5301  dmin  5302  dmiun  5303  dmuni  5304  dmopab  5305  dmi  5310  elrn  5336  rnopab  5340  dmcosseq  5357  dmres  5388  elres  5404  elsnres  5405  dfima2  5437  elima3  5442  imadmrn  5445  imai  5447  args  5462  rniun  5512  xpdifid  5531  ssrnres  5541  dmsnn0  5569  dmsnopg  5575  cnvresima  5592  mptpreima  5597  dfco2  5603  coundi  5605  coundir  5606  resco  5608  imaco  5609  rnco  5610  coiun  5614  coi1  5620  coass  5623  xpco  5644  elsnxp  5646  elsnxpOLD  5647  dffun2  5867  dffun5  5870  imadif  5941  funimaexg  5943  brprcneu  6151  dffv2  6238  fndmin  6290  fvn0ssdmfun  6316  abrexco  6467  imaiun  6468  isomin  6552  dfoprab2  6666  cbvoprab2  6693  zfun  6915  uniex2  6917  uniuni  6935  elxp4  7072  elxp5  7073  fun11iun  7088  f11o  7090  fvresex  7101  opabex3d  7106  opabex3  7107  abexssex  7110  abexex  7111  oprabrexex2  7118  releldm2  7178  dfopab2  7182  dfoprab3s  7183  fsplit  7242  frxp  7247  suppvalbr  7259  cnvimadfsn  7264  brtpos2  7318  wfrfun  7385  dfrecs3  7429  oarec  7602  oeeu  7643  domen  7928  mapsnen  7995  xpsnen  8004  xpcomco  8010  xpassen  8014  inf2  8480  zfinf  8496  axinf2  8497  zfinf2  8499  rankuni  8686  scott0  8709  cp  8714  ween  8818  aceq1  8900  aceq0  8901  aceq2  8902  dfac5lem1  8906  dfac5lem2  8907  dfac5lem3  8908  kmlem3  8934  kmlem14  8945  kmlem15  8946  kmlem16  8947  cflem  9028  cf0  9033  cfval2  9042  cfss  9047  cfslb  9048  fin23lem32  9126  axdc2lem  9230  zfac  9242  ac9  9265  ac9s  9275  axpowndlem3  9381  zfcndrep  9396  zfcndun  9397  zfcndpow  9398  zfcndinf  9400  zfcndac  9401  axgroth5  9606  axgroth2  9607  grothpw  9608  axgroth6  9610  axgroth3  9613  axgroth4  9614  grothprim  9616  grothtsk  9617  genpass  9791  ltexprlem1  9818  ltexprlem4  9821  supaddc  10950  supadd  10951  supmul1  10952  supmullem2  10954  2rexuz  11700  nnwos  11715  hashfun  13180  wwlktovfo  13651  xpcogend  13663  cbvsum  14375  cbvprod  14589  iprodmul  14678  maxprmfct  15364  4sqlem12  15603  vdwmc  15625  cshwrepswhash1  15752  imasleval  16141  isacs2  16254  cicsym  16404  gsumval3eu  18245  lidlnz  19168  isbasis2g  20692  tgval2  20700  ntreq0  20821  lmff  21045  cmpfi  21151  is1stc2  21185  1stcelcls  21204  unisngl  21270  isfbas2  21579  elfg  21615  alexsubALTlem3  21793  ustfilxp  21956  metrest  22269  metuel2  22310  restmetu  22315  cmetss  23053  dchrvmasumlema  25123  istrkg2ld  25293  istrkg3ld  25294  1loopgrvd2  26319  wlknwwlksnsur  26679  wlkwwlksur  26686  wwlksnextsur  26698  frgrwopreglem2  27074  fusgr2wsp2nb  27090  isgrpo  27239  nmo  29214  2reuswap2  29217  rexunirn  29220  disjorf  29278  fcoinvbr  29303  mpt2mptxf  29361  cnvoprab  29382  fpwrelmapffslem  29391  ordtconnlem1  29794  ddemeas  30122  omssubaddlem  30184  omssubadd  30185  eulerpartlemgvv  30261  bnj89  30548  bnj133  30554  bnj1019  30611  bnj1101  30616  bnj1109  30618  bnj1143  30622  bnj1198  30627  bnj1304  30651  bnj605  30738  bnj607  30747  bnj600  30750  bnj865  30754  bnj916  30764  bnj983  30782  bnj985  30784  bnj996  30786  bnj1033  30798  bnj1083  30807  bnj1090  30808  bnj1093  30809  bnj1110  30811  bnj1128  30819  bnj1145  30822  bnj1171  30829  bnj1172  30830  bnj1174  30832  bnj1176  30834  bnj1186  30836  bnj1189  30838  bnj1253  30846  bnj1279  30847  bnj1371  30858  bnj1374  30860  bnj1312  30887  axextprim  31339  axrepprim  31340  axunprim  31341  axpowprim  31342  axregprim  31343  axinfprim  31344  axacprim  31345  dftr6  31401  coep  31402  coepr  31403  dffr5  31404  dfpo2  31406  cnvco1  31411  cnvco2  31412  eldm3  31413  fundmpss  31421  dfdm5  31431  dfrn5  31432  elima4  31434  domep  31452  axextdfeq  31457  19.12b  31461  axextndbi  31464  frrlem5c  31540  brtxp  31682  brpprod  31687  brsset  31691  dfon3  31694  brtxpsd  31696  elfix  31705  dffix2  31707  sscoid  31715  dffun10  31716  elfuns  31717  elsingles  31720  snelsingles  31724  dfiota3  31725  brimg  31739  brapply  31740  brcup  31741  brcap  31742  brsuccf  31743  funpartlem  31744  brrestrict  31751  dfrecs2  31752  dfrdg4  31753  neifg  32061  bj-equsexval  32333  bj-dfssb2  32335  bj-eeanvw  32399  bj-clabel  32479  bj-axrep1  32484  bj-axrep4  32487  bj-axrep5  32488  bj-axsep  32489  bj-zfpow  32491  bj-cleljustab  32545  bj-denotes  32558  bj-rexvwv  32566  bj-rexcom4  32569  bj-csbsnlem  32598  bj-snsetex  32651  bj-elsngl  32656  bj-snglc  32657  bj-nul  32718  bj-restpw  32735  bj-restuni  32740  bj-dfmpt2a  32747  mptsnunlem  32856  topdifinffinlem  32866  poimirlem26  33106  ismblfin  33121  itg2addnclem3  33134  itg2addnc  33135  ismgmOLD  33320  sbcexfi  33591  sbccom2lem  33600  prtlem16  33673  prter2  33685  islshpat  33823  islpln5  34340  islvol5  34384  pmapglb  34575  polval2N  34711  cdlemftr3  35372  dibelval3  35955  dicelval3  35988  dihglb2  36150  diophrex  36858  rp-isfinite6  37384  relintab  37409  imaiun1  37463  coiun1  37464  ndisj  37584  clsk3nimkb  37859  19.36vv  38103  19.37vv  38105  pm11.58  38111  pm11.6  38113  pm13.192  38132  2sbc5g  38138  iotasbc2  38142  onfrALTlem5  38278  onfrALTlem1  38284  ax6e2nd  38295  2sb5nd  38297  en3lplem2VD  38601  relopabVD  38659  ax6e2ndVD  38666  2sb5ndVD  38668  ax6e2ndALT  38688  2sb5ndALT  38690  rfcnnnub  38717  inn0f  38764  stoweidlem34  39588  stoweidlem35  39589  stoweidlem60  39614  smfpimcc  40351  rmoanim  40513  2rmoswap  40518  sprid  41042  opeliun2xp  41429  eliunxp2  41430  setrec1lem3  41759  elpglem3  41779  eximp-surprise  41863
  Copyright terms: Public domain W3C validator