Theorem exbii 1848

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

Step	Hyp	Ref	Expression
1		exbi 1847	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1797	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 206  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2exbii  1849  3exbii  1850  exanali  1859  exancom  1861  19.43  1882  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  3exdistr  1960  19.12vvv  1994  excom13  2165  exrot4  2167  2sb5  2278  dfsb7  2279  eeor  2332  19.12vv  2345  eean  2346  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  equsexALT  2417  2sb5rf  2470  2sb8e  2528  mo4  2559  eu6lem  2566  eubii  2578  sb8eulem  2591  cbvmovw  2595  cbvmow  2596  eu1  2603  sbmo  2607  2moswapv  2622  2moswap  2637  euae  2653  issettru  2806  issetlem  2808  clabel  2874  sbabel  2924  nabbib  3028  rextru  3060  rexbii2  3072  r2exlem  3122  r19.41v  3167  r3ex  3176  r19.41  3241  rexcom4  3264  2ex2rexrot  3273  rexv  3475  cgsex4gOLD  3495  ceqsex2  3501  ceqsex2v  3502  ceqsex3v  3503  gencbvex  3507  spc3egv  3569  spc3gv  3570  ceqsrexv  3621  rexrab2  3671  euxfrw  3692  euxfr  3694  euind  3695  reu6  3697  reu3  3698  2reuswap  3717  2reuswap2  3718  reuind  3724  2reu5lem3  3728  2reu5  3729  2rmoswap  3732  sbcimdv  3822  sbcg  3826  sbccomlemOLD  3833  rmo2  3850  rmoanim  3857  rmoanimALT  3858  rexun  4159  reupick3  4293  euelss  4295  ndisj  4333  inn0f  4334  pssnel  4434  rexsns  4635  exsnrex  4644  snprc  4681  euabsn2  4689  reusn  4691  eusn  4694  elpreqpr  4831  elunirab  4886  uniprg  4887  uniun  4894  uniin  4895  uni0b  4897  uniintsn  4949  iuncom4  4964  dfiun2g  4994  dfiun2gOLD  4995  iunn0  5031  iunxiun  5061  disjor  5089  cbvopab2  5183  cbvopab2v  5186  unopab  5187  axrep1  5235  axrep4v  5239  axrep4  5240  axrep4OLD  5241  axrep5  5242  axrep6  5243  axrep6OLD  5244  zfrep4  5248  axsepgfromrep  5249  axnulALT  5259  0ex  5262  vnex  5269  inex1  5272  inuni  5305  axpweq  5306  zfpow  5321  axpow2  5322  vpwex  5332  zfpair  5376  zfpair2  5388  el  5397  eqvinop  5447  copsexgw  5450  copsexg  5451  opabn0  5513  iunopab  5519  iunopabOLD  5520  dfid2  5535  dfid3  5536  opeliunxp  5705  opeliun2xp  5706  xpiundi  5709  xpiundir  5710  elvvv  5714  csbxp  5738  eliunxp  5801  exopxfr  5807  relop  5814  opelco2g  5831  cnvco  5849  cnvuni  5850  dfdm3  5851  dfrn2  5852  dfrn3  5853  elrng  5855  dfdm4  5859  csbdm  5861  eldm2g  5863  dmun  5874  dmin  5875  dmiun  5877  dmuni  5878  dmopab  5879  dmi  5885  dmep  5887  rnep  5890  dmxp  5892  rnopab  5918  dmcosseq  5940  dmcosseqOLD  5941  dmres  5983  elsnres  5992  dfima2  6033  elima3  6038  imadmrn  6041  imai  6045  args  6063  rniun  6120  xpdifid  6141  ssrnres  6151  dmsnn0  6180  dmsnopg  6186  cnvresima  6203  mptpreima  6211  dfco2  6218  coundi  6220  coundir  6221  resco  6223  imaco  6224  rnco  6225  coiun  6229  coi1  6235  coass  6238  xpco  6262  elsnxp  6264  dfpo2  6269  dffun2OLDOLD  6523  dffun5  6528  imadif  6600  funimaexgOLD  6604  brprcneu  6848  brprcneuALT  6849  dffv2  6956  fndmin  7017  fvn0ssdmfun  7046  abrexco  7218  imaiun  7219  isomin  7312  imaeqsexvOLD  7338  dfoprab2  7447  cbvoprab2  7477  zfun  7712  uniex2  7714  uniuni  7738  elxp4  7898  elxp5  7899  fiun  7921  f1iun  7922  f11o  7925  fvresex  7938  opabex3d  7944  opabex3rd  7945  opabex3  7946  abexssex  7949  abexex  7950  oprabrexex2  7957  releldm2  8022  dfopab2  8031  dfoprab3s  8032  fsplit  8096  frxp  8105  suppvalbr  8143  cnvimadfsn  8151  brtpos2  8211  dfrecs3  8341  oarec  8526  oeeu  8567  domen  8933  xpsnen  9025  xpcomco  9031  xpassen  9035  dif1enOLD  9126  inf2  9576  zfinf  9592  axinf2  9593  zfinf2  9595  brttrcl2  9667  ttrcltr  9669  ttrclresv  9670  ttrclselem2  9679  rankuni  9816  scott0  9839  cp  9844  ween  9988  aceq1  10070  aceq0  10071  aceq2  10072  dfac5lem1  10076  dfac5lem2  10077  dfac5lem3  10078  kmlem3  10106  kmlem14  10117  kmlem15  10118  kmlem16  10119  cflem  10198  cflemOLD  10199  cf0  10204  cfval2  10213  cfss  10218  cfslb  10219  fin23lem32  10297  axdc2lem  10401  zfac  10413  ac9  10436  ac9s  10446  axpowndlem3  10552  zfcndrep  10567  zfcndun  10568  zfcndpow  10569  zfcndinf  10571  zfcndac  10572  axgroth5  10777  axgroth2  10778  axgroth6  10781  axgroth3  10784  axgroth4  10785  grothprim  10787  grothtsk  10788  genpass  10962  ltexprlem1  10989  ltexprlem4  10992  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  2rexuz  12859  nnwos  12874  hashgt23el  14389  hashfun  14402  wwlktovfo  14924  xpcogend  14940  cbvsum  15661  cbvsumv  15662  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  iprodmul  15969  maxprmfct  16679  4sqlem12  16927  vdwmc  16949  cshwrepswhash1  17073  imasleval  17504  isacs2  17614  cicsym  17766  gsumval3eu  19834  lidlnz  21152  isbasis2g  22835  tgval2  22843  ntreq0  22964  lmff  23188  cmpfi  23295  is1stc2  23329  1stcelcls  23348  unisngl  23414  isfbas2  23722  elfg  23758  alexsubALTlem3  23936  ustfilxp  24100  metrest  24412  metuel2  24453  restmetu  24458  dchrvmasumlema  27411  elold  27781  lrrecfr  27850  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  renegscl  28349  readdscl  28350  remulscl  28353  istrkg2ld  28387  istrkg3ld  28388  1loopgrvd2  29431  wwlksnextsurj  29830  isgrpo  30426  nmo  32419  reuxfrdf  32420  rexunirn  32421  dmrab  32426  disjorf  32508  fcoinvbr  32534  mpomptxf  32601  fpwrelmapffslem  32655  1arithidom  33508  ordtconnlem1  33914  ddemeas  34226  omssubaddlem  34290  omssubadd  34291  eulerpartlemgvv  34367  bnj89  34711  bnj133  34717  bnj1019  34769  bnj1101  34774  bnj1109  34776  bnj1143  34780  bnj1198  34785  bnj1304  34809  bnj605  34897  bnj607  34906  bnj600  34909  bnj865  34913  bnj916  34923  bnj983  34941  bnj985v  34943  bnj985  34944  bnj996  34946  bnj1033  34959  bnj1083  34968  bnj1090  34969  bnj1093  34970  bnj1110  34972  bnj1128  34980  bnj1145  34983  bnj1171  34990  bnj1172  34991  bnj1174  34993  bnj1176  34995  bnj1186  34997  bnj1189  34999  bnj1253  35007  bnj1279  35008  bnj1371  35019  bnj1374  35021  bnj1312  35048  exdifsn  35069  fineqvrep  35085  fineqvpow  35086  lfuhgr3  35107  loop1cycl  35124  satfvsucsuc  35352  satf0op  35364  axextprim  35688  axrepprim  35689  axunprim  35690  axpowprim  35691  axregprim  35692  axinfprim  35693  axacprim  35694  dftr6  35738  coep  35739  coepr  35740  dffr5  35741  cnvco1  35746  cnvco2  35747  eldm3  35748  fundmpss  35754  dfdm5  35760  dfrn5  35761  elima4  35763  axextdfeq  35785  19.12b  35789  axextndbi  35792  brtxp  35868  brpprod  35873  brsset  35877  dfon3  35880  brtxpsd  35882  elfix  35891  dffix2  35893  sscoid  35901  dffun10  35902  elfuns  35903  elsingles  35906  snelsingles  35910  dfiota3  35911  brimg  35925  brapply  35926  brcup  35927  brcap  35928  brsuccf  35929  funpartlem  35930  brrestrict  35937  dfrecs2  35938  dfrdg4  35939  sumeq2si  36190  prodeq2si  36192  cbvoprab2vw  36226  cbvoprab23vw  36228  cbvprodvw2  36235  neifg  36359  bj-equsexval  36648  bj-eeanvw  36701  bj-substw  36710  eliminable-abelv  36857  eliminable-abelab  36858  bj-denoteslem  36859  bj-rexvw  36868  bj-csbsnlem  36891  bj-gabima  36928  bj-snsetex  36951  bj-elsngl  36956  bj-snglc  36957  bj-abex  37018  bj-clex  37019  bj-clel3gALT  37036  bj-nul  37044  bj-dfid2ALT  37053  bj-restpw  37080  bj-restuni  37085  bj-dfmpoa  37106  bj-opabco  37176  bj-xpcossxp  37177  bj-imdirco  37178  mptsnunlem  37326  topdifinffinlem  37335  difunieq  37362  wl-dfclab  37584  poimirlem26  37640  ismblfin  37655  itg2addnclem3  37667  itg2addnc  37668  ismgmOLD  37844  sbcexfi  38111  sbccom2lem  38118  eldmres  38259  ecinn0  38335  ineleq  38336  moantr  38346  dmcnvep  38361  rnxrn  38384  rnxrnres  38385  dfcoss2  38404  dfcoss3  38405  cosscnv  38407  coss1cnvres  38408  coss2cnvepres  38409  1cossres  38420  cocossss  38427  rncossdmcoss  38446  eldmcoss2  38450  coss0  38470  cossid  38471  dfssr2  38490  eldmqs1cossres  38651  prtlem16  38862  prter2  38874  islshpat  39010  islpln5  39529  islvol5  39573  pmapglb  39764  polval2N  39900  cdlemftr3  40559  dibelval3  41141  dicelval3  41174  dihglb2  41336  sn-axrep5v  42204  prjspeclsp  42600  euabsn2w  42667  diophrex  42763  onsupmaxb  43228  nnoeomeqom  43301  tfsconcatlem  43325  tfsconcat0i  43334  rp-isfinite6  43507  snen1g  43513  relintab  43572  imaiun1  43640  coiun1  43641  clsk3nimkb  44029  expandexn  44278  ismnuprim  44283  rr-groth  44288  ismnushort  44290  rr-grothshortbi  44292  19.36vv  44372  19.37vv  44374  pm11.58  44379  pm11.6  44381  pm13.192  44399  2sbc5g  44405  iotasbc2  44409  onfrALTlem5  44532  onfrALTlem1  44538  ax6e2nd  44548  2sb5nd  44550  en3lplem2VD  44833  onfrALTlem5VD  44874  relopabVD  44890  ax6e2ndVD  44897  2sb5ndVD  44899  ax6e2ndALT  44919  2sb5ndALT  44921  dfac5prim  44980  brpermmodel  44993  permaxrep  44996  permac8prim  45004  rfcnnnub  45030  stoweidlem34  46032  stoweidlem35  46033  stoweidlem60  46058  smfpimcc  46806  ichexmpl1  47470  sprid  47475  dfgric2  47915  usgrgrtrirex  47949  grlimgrtri  47995  eliunxp2  48322  mosssn2  48805  coxp  48821  istermc  49463  setrec1lem3  49678  elpglem3  49702  eximp-surprise  49773