Theorem exbii 1851

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 1850	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1800	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 205  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2exbii  1852  3exbii  1853  exanali  1863  exancom  1865  19.43  1886  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1959  exdistr2  1963  3exdistr  1965  19.12vvv  1993  excom13  2165  exrot4  2167  2sb5  2272  dfsb7  2276  eeor  2330  eeorOLD  2331  19.12vv  2344  eean  2345  eeeanv  2347  ee4anv  2348  2sb8ef  2353  equsexALT  2419  2sb5rf  2472  2sb8e  2530  mo4  2561  eu6lem  2568  eubii  2580  sb8eulem  2593  cbvmovw  2597  cbvmow  2598  eu1  2607  sbmo  2611  2moswapv  2626  2moswap  2641  euae  2656  issetlem  2814  clabel  2882  sbabel  2939  sbabelOLD  2940  nabbib  3046  rextru  3078  rexbii2  3091  r2exlem  3144  r19.41v  3189  r19.41  3261  rexcom4  3286  rexcomOLD  3289  2ex2rexrot  3296  rexv  3500  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  ceqsex2  3530  ceqsex2v  3531  ceqsex3v  3532  gencbvex  3536  spc3egv  3594  spc3gv  3595  ceqsrexv  3644  rexabOLD  3692  rexrab2  3697  euxfrw  3718  euxfr  3720  euind  3721  reu6  3723  reu3  3724  2reuswap  3743  2reuswap2  3744  reuind  3750  2reu5lem3  3754  2reu5  3755  2rmoswap  3758  sbcimdv  3852  sbcg  3857  sbccomlem  3865  rmo2  3882  rmoanim  3889  rmoanimALT  3890  rexun  4191  reupick3  4320  euelss  4322  ndisj  4368  abn0OLD  4382  pssnel  4471  rexsns  4674  exsnrex  4685  snprc  4722  euabsn2  4730  reusn  4732  eusn  4735  elpreqpr  4868  elunirab  4925  uniprg  4926  uniprOLD  4928  uniun  4935  uniin  4936  uni0b  4938  uniintsn  4992  iuncom4  5006  dfiun2g  5034  dfiun2gOLD  5035  iunn0  5071  iunxiun  5101  disjor  5129  cbvopab2  5226  cbvopab2v  5230  unopab  5231  axrep1  5287  axrep4  5291  axrep5  5292  axrep6  5293  zfrep4  5297  axsepgfromrep  5298  axnulALT  5305  0ex  5308  vnex  5315  inex1  5318  inuni  5344  axpweq  5349  zfpow  5365  axpow2  5366  axpow3  5367  vpwex  5376  zfpair  5420  zfpair2  5429  el  5438  eqvinop  5488  copsexgw  5491  copsexg  5492  opabn0  5554  iunopab  5560  iunopabOLD  5561  dfid2  5577  dfid3  5578  opeliunxp  5744  xpiundi  5747  xpiundir  5748  elvvv  5752  csbxp  5776  eliunxp  5838  exopxfr  5844  relop  5851  opelco2g  5868  cnvco  5886  cnvuni  5887  dfdm3  5888  dfrn2  5889  dfrn3  5890  elrng  5892  dfdm4  5896  csbdm  5898  eldm2g  5900  dmun  5911  dmin  5912  dmiun  5914  dmuni  5915  dmopab  5916  dmi  5922  dmep  5924  rnep  5927  rnopab  5954  dmcosseq  5973  dmres  6004  elsnres  6022  dfima2  6062  elima3  6067  imadmrn  6070  imai  6074  args  6092  rniun  6148  xpdifid  6168  ssrnres  6178  dmsnn0  6207  dmsnopg  6213  cnvresima  6230  mptpreima  6238  dfco2  6245  coundi  6247  coundir  6248  resco  6250  imaco  6251  rnco  6252  coiun  6256  coi1  6262  coass  6265  xpco  6289  elsnxp  6291  dfpo2  6296  dffun2OLDOLD  6556  dffun5  6561  imadif  6633  funimaexgOLD  6636  brprcneu  6882  brprcneuALT  6883  dffv2  6987  fndmin  7047  fvn0ssdmfun  7077  abrexco  7243  imaiun  7244  isomin  7334  imaeqsexv  7360  dfoprab2  7467  cbvoprab2  7497  zfun  7726  uniex2  7728  uniuni  7749  elxp4  7913  elxp5  7914  fiun  7929  f1iun  7930  f11o  7933  fvresex  7946  opabex3d  7952  opabex3rd  7953  opabex3  7954  abexssex  7957  abexex  7958  oprabrexex2  7965  releldm2  8029  dfopab2  8038  dfoprab3s  8039  fsplit  8103  frxp  8112  suppvalbr  8150  cnvimadfsn  8157  brtpos2  8217  dfwrecsOLD  8298  wfrfunOLD  8319  dfrecs3  8372  dfrecs3OLD  8373  oarec  8562  oeeu  8603  domen  8957  xpsnen  9055  xpcomco  9062  xpassen  9066  dif1enOLD  9162  inf2  9618  zfinf  9634  axinf2  9635  zfinf2  9637  brttrcl2  9709  ttrcltr  9711  ttrclresv  9712  ttrclselem2  9721  rankuni  9858  scott0  9881  cp  9886  ween  10030  aceq1  10112  aceq0  10113  aceq2  10114  dfac5lem1  10118  dfac5lem2  10119  dfac5lem3  10120  kmlem3  10147  kmlem14  10158  kmlem15  10159  kmlem16  10160  cflem  10241  cf0  10246  cfval2  10255  cfss  10260  cfslb  10261  fin23lem32  10339  axdc2lem  10443  zfac  10455  ac9  10478  ac9s  10488  axpowndlem3  10594  zfcndrep  10609  zfcndun  10610  zfcndpow  10611  zfcndinf  10613  zfcndac  10614  axgroth5  10819  axgroth2  10820  axgroth6  10823  axgroth3  10826  axgroth4  10827  grothprim  10829  grothtsk  10830  genpass  11004  ltexprlem1  11031  ltexprlem4  11034  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  2rexuz  12884  nnwos  12899  hashgt23el  14384  hashfun  14397  wwlktovfo  14909  xpcogend  14921  cbvsum  15641  cbvprod  15859  iprodmul  15947  maxprmfct  16646  4sqlem12  16889  vdwmc  16911  cshwrepswhash1  17036  imasleval  17487  isacs2  17597  cicsym  17751  gsumval3eu  19772  lidlnz  20853  isbasis2g  22451  tgval2  22459  ntreq0  22581  lmff  22805  cmpfi  22912  is1stc2  22946  1stcelcls  22965  unisngl  23031  isfbas2  23339  elfg  23375  alexsubALTlem3  23553  ustfilxp  23717  metrest  24033  metuel2  24074  restmetu  24079  dchrvmasumlema  27003  elold  27364  lrrecfr  27427  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  mulsuniflem  27604  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  istrkg2ld  27711  istrkg3ld  27712  1loopgrvd2  28760  wwlksnextsurj  29154  isgrpo  29750  nmo  31730  reuxfrdf  31731  rexunirn  31732  dmrab  31737  disjorf  31810  fcoinvbr  31836  mpomptxf  31905  cnvoprabOLD  31945  fpwrelmapffslem  31957  ordtconnlem1  32904  ddemeas  33234  omssubaddlem  33298  omssubadd  33299  eulerpartlemgvv  33375  bnj89  33732  bnj133  33738  bnj1019  33790  bnj1101  33795  bnj1109  33797  bnj1143  33801  bnj1198  33806  bnj1304  33830  bnj605  33918  bnj607  33927  bnj600  33930  bnj865  33934  bnj916  33944  bnj983  33962  bnj985v  33964  bnj985  33965  bnj996  33967  bnj1033  33980  bnj1083  33989  bnj1090  33990  bnj1093  33991  bnj1110  33993  bnj1128  34001  bnj1145  34004  bnj1171  34011  bnj1172  34012  bnj1174  34014  bnj1176  34016  bnj1186  34018  bnj1189  34020  bnj1253  34028  bnj1279  34029  bnj1371  34040  bnj1374  34042  bnj1312  34069  exdifsn  34084  fineqvrep  34095  fineqvpow  34096  lfuhgr3  34110  loop1cycl  34128  satfvsucsuc  34356  satf0op  34368  axextprim  34670  axrepprim  34671  axunprim  34672  axpowprim  34673  axregprim  34674  axinfprim  34675  axacprim  34676  dftr6  34721  coep  34722  coepr  34723  dffr5  34724  cnvco1  34729  cnvco2  34730  eldm3  34731  fundmpss  34738  dfdm5  34744  dfrn5  34745  elima4  34747  axextdfeq  34769  19.12b  34773  axextndbi  34776  brtxp  34852  brpprod  34857  brsset  34861  dfon3  34864  brtxpsd  34866  elfix  34875  dffix2  34877  sscoid  34885  dffun10  34886  elfuns  34887  elsingles  34890  snelsingles  34894  dfiota3  34895  brimg  34909  brapply  34910  brcup  34911  brcap  34912  brsuccf  34913  funpartlem  34914  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  neifg  35256  bj-equsexval  35537  bj-eeanvw  35591  bj-substw  35600  eliminable-abelv  35748  eliminable-abelab  35749  bj-denoteslem  35750  bj-rexvw  35760  bj-csbsnlem  35783  bj-gabima  35820  bj-snsetex  35844  bj-elsngl  35849  bj-snglc  35850  bj-abex  35911  bj-clex  35912  bj-clel3gALT  35929  bj-nul  35937  bj-dfid2ALT  35946  bj-restpw  35973  bj-restuni  35978  bj-dfmpoa  35999  bj-opabco  36069  bj-xpcossxp  36070  bj-imdirco  36071  mptsnunlem  36219  topdifinffinlem  36228  difunieq  36255  wl-dfclab  36458  poimirlem26  36514  ismblfin  36529  itg2addnclem3  36541  itg2addnc  36542  ismgmOLD  36718  sbcexfi  36985  sbccom2lem  36992  eldmres  37138  ecinn0  37222  ineleq  37223  moantr  37233  rnxrn  37268  rnxrnres  37269  dfcoss2  37283  dfcoss3  37284  cosscnv  37286  coss1cnvres  37287  coss2cnvepres  37288  1cossres  37299  cocossss  37306  rncossdmcoss  37325  eldmcoss2  37329  coss0  37349  cossid  37350  dfssr2  37369  eldmqs1cossres  37529  prtlem16  37739  prter2  37751  islshpat  37887  islpln5  38406  islvol5  38450  pmapglb  38641  polval2N  38777  cdlemftr3  39436  dibelval3  40018  dicelval3  40051  dihglb2  40213  sn-axrep5v  41033  prjspeclsp  41354  diophrex  41513  onsupmaxb  41988  nnoeomeqom  42062  tfsconcatlem  42086  tfsconcat0i  42095  rp-isfinite6  42269  snen1g  42275  relintab  42334  imaiun1  42402  coiun1  42403  clsk3nimkb  42791  expandexn  43048  ismnuprim  43053  rr-groth  43058  ismnushort  43060  rr-grothshortbi  43062  19.36vv  43142  19.37vv  43144  pm11.58  43149  pm11.6  43151  pm13.192  43169  2sbc5g  43175  iotasbc2  43179  onfrALTlem5  43303  onfrALTlem1  43309  ax6e2nd  43319  2sb5nd  43321  en3lplem2VD  43605  onfrALTlem5VD  43646  relopabVD  43662  ax6e2ndVD  43669  2sb5ndVD  43671  ax6e2ndALT  43691  2sb5ndALT  43693  rfcnnnub  43720  inn0f  43760  stoweidlem34  44750  stoweidlem35  44751  stoweidlem60  44776  smfpimcc  45524  ichexmpl1  46137  sprid  46142  opeliun2xp  47008  eliunxp2  47009  mosssn2  47501  setrec1lem3  47734  elpglem3  47758  eximp-surprise  47831