Theorem exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1780

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

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

This theorem is referenced by:  2exbii  1850  3exbii  1851  exanali  1860  exancom  1862  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  3exdistr  1961  19.12vvv  1995  excom13  2169  exrot4  2171  2sb5  2282  dfsb7  2283  eeor  2336  19.12vv  2349  eean  2350  eeeanv  2352  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2358  equsexALT  2421  2sb5rf  2474  2sb8e  2532  mo4  2563  eu6lem  2570  eubii  2582  sb8eulem  2595  cbvmovw  2599  cbvmow  2600  eu1  2607  sbmo  2611  2moswapv  2626  2moswap  2641  euae  2657  issettru  2811  issetlem  2813  clabel  2878  sbabel  2928  nabbib  3032  rextru  3064  rexbii2  3076  r2exlem  3122  r19.41v  3163  r3ex  3172  r19.41  3237  rexcom4  3260  2ex2rexrot  3268  rexv  3465  cgsex4gOLD  3485  ceqsex2  3490  ceqsex2v  3491  ceqsex3v  3492  gencbvex  3496  spc3egv  3554  spc3gv  3555  ceqsrexv  3606  rexrab2  3655  euxfrw  3676  euxfr  3678  euind  3679  reu6  3681  reu3  3682  2reuswap  3701  2reuswap2  3702  reuind  3708  2reu5lem3  3712  2reu5  3713  2rmoswap  3716  sbcimdv  3806  sbcg  3810  sbccomlemOLD  3817  rmo2  3834  rmoanim  3841  rmoanimALT  3842  rexun  4145  reupick3  4279  euelss  4281  ndisj  4319  inn0f  4320  pssnel  4420  rexsns  4625  exsnrex  4634  snprc  4671  euabsn2  4679  reusn  4681  eusn  4684  elpreqpr  4820  elunirab  4875  uniprg  4876  uniun  4883  uniin  4884  uni0b  4886  uniintsn  4937  iuncom4  4952  dfiun2g  4982  iunn0  5019  iunxiun  5049  disjor  5077  cbvopab2  5171  cbvopab2v  5174  unopab  5175  axrep1  5222  axrep4v  5226  axrep4  5227  axrep4OLD  5228  axrep5  5229  axrep6  5230  axrep6OLD  5231  zfrep4  5235  axsepgfromrep  5236  axnulALT  5246  0ex  5249  vnex  5256  inex1  5259  inuni  5292  axpweq  5293  zfpow  5308  axpow2  5309  vpwex  5319  zfpair  5363  zfpair2  5375  el  5384  eqvinop  5432  copsexgw  5435  copsexg  5436  opabn0  5498  iunopab  5504  dfid2  5518  dfid3  5519  opeliunxp  5688  opeliun2xp  5689  xpiundi  5692  xpiundir  5693  elvvv  5697  csbxp  5722  eliunxp  5783  exopxfr  5789  relop  5796  opelco2g  5813  cnvco  5831  cnvuni  5832  dfdm3  5833  dfrn2  5834  dfrn3  5835  elrng  5837  dfdm4  5841  csbdm  5843  eldm2g  5845  dmun  5856  dmin  5857  dmiun  5859  dmuni  5860  dmopab  5861  dmi  5867  dmep  5869  rnep  5873  dmxp  5875  rnopab  5900  dmcosseq  5924  dmcosseqOLD  5925  dmcosseqOLDOLD  5926  dmres  5968  elsnres  5977  dfima2  6018  elima3  6023  imadmrn  6026  imai  6030  args  6048  rniun  6102  xpdifid  6123  ssrnres  6133  dmsnn0  6162  dmsnopg  6168  cnvresima  6185  mptpreima  6193  dfco2  6200  coundi  6202  coundir  6203  resco  6205  imaco  6206  rnco  6207  rncoOLD  6208  coiun  6212  coi1  6218  coass  6221  xpco  6244  elsnxp  6246  dfpo2  6251  dffun5  6503  imadif  6573  tz6.12-2  6818  brprcneu  6821  brprcneuALT  6822  dffv2  6926  fndmin  6987  fvn0ssdmfun  7016  abrexco  7187  imaiun  7188  isomin  7280  imaeqsexvOLD  7306  dfoprab2  7413  cbvoprab2  7443  zfun  7678  uniex2  7680  uniuni  7704  elxp4  7861  elxp5  7862  fiun  7884  f1iun  7885  f11o  7888  fvresex  7901  opabex3d  7906  opabex3rd  7907  opabex3  7908  abexssex  7911  abexex  7912  oprabrexex2  7919  releldm2  7984  dfopab2  7993  dfoprab3s  7994  fsplit  8056  frxp  8065  suppvalbr  8103  cnvimadfsn  8111  brtpos2  8171  dfrecs3  8301  oarec  8486  oeeu  8527  domen  8894  xpsnen  8985  xpcomco  8991  xpassen  8995  inf2  9524  zfinf  9540  axinf2  9541  zfinf2  9543  brttrcl2  9615  ttrcltr  9617  ttrclresv  9618  ttrclselem2  9627  rankuni  9767  scott0  9790  cp  9795  ween  9937  aceq1  10019  aceq0  10020  aceq2  10021  dfac5lem1  10025  dfac5lem2  10026  dfac5lem3  10027  kmlem3  10055  kmlem14  10066  kmlem15  10067  kmlem16  10068  cflem  10147  cflemOLD  10148  cf0  10153  cfval2  10162  cfss  10167  cfslb  10168  fin23lem32  10246  axdc2lem  10350  zfac  10362  ac9  10385  ac9s  10395  axpowndlem3  10501  zfcndrep  10516  zfcndun  10517  zfcndpow  10518  zfcndinf  10520  zfcndac  10521  axgroth5  10726  axgroth2  10727  axgroth6  10730  axgroth3  10733  axgroth4  10734  grothprim  10736  grothtsk  10737  genpass  10911  ltexprlem1  10938  ltexprlem4  10941  supaddc  12100  supadd  12101  supmul1  12102  supmullem2  12104  2rexuz  12804  nnwos  12819  hashgt23el  14338  hashfun  14351  wwlktovfo  14872  xpcogend  14888  cbvsum  15609  cbvsumv  15610  cbvprod  15827  cbvprodv  15828  prodeq1i  15830  iprodmul  15917  maxprmfct  16627  4sqlem12  16875  vdwmc  16897  cshwrepswhash1  17021  imasleval  17453  isacs2  17567  cicsym  17719  gsumval3eu  19824  lidlnz  21188  isbasis2g  22883  tgval2  22891  ntreq0  23012  lmff  23236  cmpfi  23343  is1stc2  23377  1stcelcls  23396  unisngl  23462  isfbas2  23770  elfg  23806  alexsubALTlem3  23984  ustfilxp  24148  metrest  24459  metuel2  24500  restmetu  24505  dchrvmasumlema  27458  elold  27834  lrrecfr  27906  sleadd1  27952  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  mulsuniflem  28108  addsdilem1  28110  addsdilem2  28111  mulsasslem1  28122  mulsasslem2  28123  renegscl  28420  readdscl  28421  remulscl  28424  istrkg2ld  28458  istrkg3ld  28459  1loopgrvd2  29503  wwlksnextsurj  29899  isgrpo  30498  nmo  32490  reuxfrdf  32491  rexunirn  32492  dmrab  32497  disjorf  32580  fcoinvbr  32606  mpomptxf  32683  fpwrelmapffslem  32739  1arithidom  33546  ordtconnlem1  34009  ddemeas  34321  omssubaddlem  34384  omssubadd  34385  eulerpartlemgvv  34461  bnj89  34805  bnj133  34811  bnj1019  34863  bnj1101  34868  bnj1109  34870  bnj1143  34874  bnj1198  34879  bnj1304  34903  bnj605  34991  bnj607  35000  bnj600  35003  bnj865  35007  bnj916  35017  bnj983  35035  bnj985v  35037  bnj985  35038  bnj996  35040  bnj1033  35053  bnj1083  35062  bnj1090  35063  bnj1093  35064  bnj1110  35066  bnj1128  35074  bnj1145  35077  bnj1171  35084  bnj1172  35085  bnj1174  35087  bnj1176  35089  bnj1186  35091  bnj1189  35093  bnj1253  35101  bnj1279  35102  bnj1371  35113  bnj1374  35115  bnj1312  35142  exdifsn  35163  axreg  35197  axregscl  35198  fineqvrep  35209  fineqvpow  35210  axregs  35217  lfuhgr3  35236  loop1cycl  35253  satfvsucsuc  35481  satf0op  35493  axextprim  35817  axrepprim  35818  axunprim  35819  axpowprim  35820  axregprim  35821  axinfprim  35822  axacprim  35823  dftr6  35867  coep  35868  coepr  35869  dffr5  35870  cnvco1  35875  cnvco2  35876  eldm3  35877  fundmpss  35883  dfdm5  35889  dfrn5  35890  elima4  35892  axextdfeq  35911  19.12b  35915  axextndbi  35918  brtxp  35994  brpprod  35999  brsset  36003  dfon3  36006  brtxpsd  36008  elfix  36017  dffix2  36019  sscoid  36027  dffun10  36028  elfuns  36029  elsingles  36032  snelsingles  36036  dfiota3  36037  brimg  36051  brapply  36052  brcup  36053  brcap  36054  lemsuccf  36055  funpartlem  36058  brrestrict  36065  dfrecs2  36066  dfrdg4  36067  sumeq2si  36318  prodeq2si  36320  cbvoprab2vw  36354  cbvoprab23vw  36356  cbvprodvw2  36363  neifg  36487  bj-df-sb  36769  bj-equsexval  36777  bj-eeanvw  36830  bj-substw  36839  eliminable-abelv  36986  eliminable-abelab  36987  bj-denoteslem  36988  bj-rexvw  36997  bj-csbsnlem  37020  bj-gabima  37057  bj-snsetex  37080  bj-elsngl  37085  bj-snglc  37086  bj-abex  37147  bj-clex  37148  bj-clel3gALT  37165  bj-nul  37173  bj-dfid2ALT  37182  bj-restpw  37209  bj-restuni  37214  bj-dfmpoa  37235  bj-opabco  37305  bj-xpcossxp  37306  bj-imdirco  37307  mptsnunlem  37455  topdifinffinlem  37464  difunieq  37491  wl-dfclab  37702  poimirlem26  37759  ismblfin  37774  itg2addnclem3  37786  itg2addnc  37787  ismgmOLD  37963  sbcexfi  38230  sbccom2lem  38237  eldmres  38382  ecinn0  38458  ineleq  38459  moantr  38469  dmcnvep  38485  rnxrn  38518  rnxrnres  38519  dmsucmap  38554  dfcoss2  38588  dfcoss3  38589  cosscnv  38591  coss1cnvres  38592  coss2cnvepres  38593  1cossres  38604  cocossss  38611  rncossdmcoss  38630  eldmcoss2  38634  coss0  38654  cossid  38655  dfssr2  38664  eldmqs1cossres  38830  prtlem16  39041  prter2  39053  islshpat  39189  islpln5  39707  islvol5  39751  pmapglb  39942  polval2N  40078  cdlemftr3  40737  dibelval3  41319  dicelval3  41352  dihglb2  41514  sn-axrep5v  42387  prjspeclsp  42770  euabsn2w  42837  diophrex  42932  onsupmaxb  43396  nnoeomeqom  43469  tfsconcatlem  43493  tfsconcat0i  43502  rp-isfinite6  43675  snen1g  43681  relintab  43740  imaiun1  43808  coiun1  43809  clsk3nimkb  44197  expandexn  44446  ismnuprim  44451  rr-groth  44456  ismnushort  44458  rr-grothshortbi  44460  19.36vv  44540  19.37vv  44542  pm11.58  44547  pm11.6  44549  pm13.192  44567  2sbc5g  44573  iotasbc2  44577  onfrALTlem5  44699  onfrALTlem1  44705  ax6e2nd  44715  2sb5nd  44717  en3lplem2VD  45000  onfrALTlem5VD  45041  relopabVD  45057  ax6e2ndVD  45064  2sb5ndVD  45066  ax6e2ndALT  45086  2sb5ndALT  45088  dfac5prim  45147  brpermmodel  45160  permaxrep  45163  permac8prim  45171  rfcnnnub  45197  stoweidlem34  46194  stoweidlem35  46195  stoweidlem60  46220  smfpimcc  46968  ichexmpl1  47631  sprid  47636  dfgric2  48077  usgrgrtrirex  48112  grlimgrtri  48165  eliunxp2  48496  mosssn2  48978  coxp  48994  istermc  49635  setrec1lem3  49850  elpglem3  49874  eximp-surprise  49945