Theorem exbii 1875

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

Syntax hints:   ↔ wb 209  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  2exbii  1876  3exbii  1877  exanali  1886  exancom  1888  19.43  1909  19.41vv  1977  19.41vvv  1978  19.41vvvv  1979  exdistr  1981  exdistr2  1985  3exdistr  1987  19.12vvv  2021  excom13  2205  exrot4  2207  2sb5  2319  dfsb7  2320  eeor  2372  19.12vv  2385  eean  2386  eeeanv  2388  ee4anv  2389  ee4anvOLD  2390  2sb8ef  2394  equsexALT  2457  2sb5rf  2510  2sb8e  2568  mo4  2600  eu6lem  2607  sb8eulem  2632  cbvmovw  2636  cbvmow  2637  eu1  2644  sbmo  2648  2moswapv  2663  2moswap  2678  euae  2693  issettru  2847  issetlem  2849  clabel  2914  sbabel  2963  nabbib  3069  rextru  3102  rexbii2  3114  r2exlem  3160  r19.41v  3201  r3ex  3210  r19.41  3275  rexcom4  3298  2ex2rexrot  3306  rexv  3490  ceqsex2  3513  ceqsex2v  3514  ceqsex3v  3515  gencbvex  3519  spc3egv  3571  spc3gv  3572  ceqsrexv  3623  rexrab2  3672  euxfrw  3693  euxfr  3695  euind  3696  reu6  3698  reu3  3699  2reuswap  3718  2reuswap2  3719  reuind  3725  2reu5lem3  3729  2reu5  3730  2rmoswap  3733  sbcimdv  3821  sbcg  3825  sbccomlemOLD  3832  rmo2  3849  rmoanim  3856  rmoanimALT  3857  rexun  4157  reupick3  4291  euelss  4293  ndisj  4332  inn0f  4333  pssnel  4434  rexsns  4639  exsnrex  4648  snprc  4685  euabsn2  4693  reusn  4695  eusn  4698  elpreqpr  4833  elunirab  4888  uniprg  4889  uniun  4896  uniinOLD  4898  uni0b  4900  uniintsn  4951  iuncom4  4966  dfiun2g  4995  iunn0  5032  iunxiun  5064  disjor  5092  cbvopab2  5188  cbvopab2v  5191  unopab  5192  axrep1  5240  axrep4v  5244  axrep4  5245  axrep4OLD  5246  axrep5  5247  axrep6  5248  axrep6OLD  5249  zfrep6  5251  zfrep4  5255  axsepgfromrep  5256  axnulALT  5266  0ex  5269  vnexOLD  5280  inex1  5285  inuni  5318  axpweq  5319  zfpow  5335  axpow2  5336  vpwex  5346  zfpair  5390  zfpair2  5403  prex  5407  elOLD  5418  eqvinop  5467  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  opabn0  5536  iunopab  5542  dfid2  5556  dfid3  5557  opeliunxp  5726  opeliun2xp  5727  xpiundi  5730  xpiundir  5731  elvvv  5735  csbxp  5760  eliunxp  5821  exopxfr  5827  relop  5834  opelco2g  5851  cnvco  5873  cnvuni  5874  dfdm3  5875  dfrn2  5876  dfrn3  5877  elrng  5879  dfdm4  5883  csbdm  5885  eldm2g  5887  dmun  5898  dmin  5899  dmiun  5901  dmuni  5902  dmopab  5903  dmi  5909  dmep  5911  rnep  5915  dmxp  5917  rnopab  5942  dmcosseq  5966  dmcosseqOLD  5967  dmres  6009  elsnres  6018  dfima2  6062  elima3  6067  imadmrn  6070  imai  6074  args  6092  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  ssrnres  6175  dmsnn0  6205  dmsnopg  6211  cnvresima  6228  mptpreima  6236  dfco2  6243  coundi  6245  coundir  6246  resco  6248  imaco  6249  rnco  6250  rncoOLD  6251  coiun  6255  coi1  6261  coass  6264  xpco  6287  elsnxp  6289  dfpo2  6294  dffun5  6547  imadif  6617  tz6.12-2  6866  brprcneu  6869  brprcneuALT  6870  dffv2  6974  fndmin  7038  fvn0ssdmfun  7067  abrexco  7240  imaiun  7241  isomin  7333  imaeqsexvOLD  7359  dfoprab2  7466  cbvoprab2  7496  zfun  7731  uniex2  7733  uniuni  7757  elxp4  7915  elxp5  7916  fiun  7936  f1iun  7937  f11o  7940  fvresex  7953  opabex3d  7958  opabex3rd  7959  opabex3  7960  abexssex  7963  abexex  7964  oprabrexex2  7971  releldm2  8036  dfopab2  8045  dfoprab3s  8046  fsplit  8108  frxp  8118  suppvalbr  8156  cnvimadfsn  8164  brtpos2  8224  dfrecs3  8355  oarec  8543  oeeu  8585  domen  8954  xpsnen  9045  xpcomco  9051  xpassen  9055  inf2  9588  zfinf  9604  axinf2  9605  zfinf2  9607  brttrcl2  9679  ttrcltr  9681  ttrclresv  9682  ttrclselem2  9691  rankuni  9831  scott0  9856  cp  9873  ween  10015  aceq1  10097  aceq0  10098  aceq2  10099  dfac5lem1  10103  dfac5lem2  10104  dfac5lem3  10105  kmlem3  10132  kmlem14  10143  kmlem15  10144  kmlem16  10145  cflem  10224  cflemOLD  10225  cf0  10230  cfval2  10240  cfss  10245  cfslb  10246  fin23lem32  10324  axdc2lem  10428  zfac  10440  ac9  10463  ac9s  10473  axpowndlem3  10580  zfcndrep  10595  zfcndun  10596  zfcndpow  10597  zfcndinf  10599  zfcndac  10600  axgroth5  10805  axgroth2  10806  axgroth6  10809  axgroth3  10812  axgroth4  10813  grothprim  10815  grothtsk  10816  genpass  10990  ltexprlem1  11017  ltexprlem4  11020  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  2rexuz  12920  nnwos  12935  hashgt23el  14457  hashfun  14470  wwlktovfo  14991  xpcogend  15007  cbvsum  15742  cbvsumv  15743  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  iprodmul  16053  maxprmfct  16764  4sqlem12  17012  vdwmc  17034  cshwrepswhash1  17158  imasleval  17591  isacs2  17705  cicsym  17857  gsumval3eu  19970  lidlnz  21346  isbasis2g  23070  tgval2  23078  ntreq0  23199  lmff  23423  cmpfi  23530  is1stc2  23564  1stcelcls  23583  unisngl  23649  isfbas2  23957  elfg  23993  alexsubALTlem3  24171  ustfilxp  24335  metrest  24646  metuel2  24687  restmetu  24692  dchrvmasumlema  27626  elold  28014  lrrecfr  28098  leadds1  28144  addsuniflem  28156  addsasslem1  28158  addsasslem2  28159  mulsuniflem  28304  addsdilem1  28306  addsdilem2  28307  mulsasslem1  28318  mulsasslem2  28319  elreno2  28650  renegscl  28653  readdscl  28654  remulscl  28657  istrkg2ld  28691  istrkg3ld  28692  1loopgrvd2  29790  wwlksnextsurj  30186  isgrpo  30786  nmo  32773  reuxfrdf  32774  rexunirn  32775  dmrab  32780  disjorf  32861  fcoinvbr  32887  mpomptxf  32960  fpwrelmapffslem  33014  1arithidom  33768  ordtconnlem1  34255  ddemeas  34567  omssubaddlem  34630  omssubadd  34631  eulerpartlemgvv  34707  bnj89  35051  bnj133  35057  bnj1019  35109  bnj1101  35114  bnj1109  35116  bnj1143  35119  bnj1198  35124  bnj1304  35148  bnj605  35236  bnj607  35245  bnj600  35248  bnj865  35252  bnj916  35262  bnj983  35280  bnj985v  35282  bnj985  35283  bnj996  35285  bnj1033  35298  bnj1083  35307  bnj1090  35308  bnj1093  35309  bnj1110  35311  bnj1128  35319  bnj1145  35322  bnj1171  35329  bnj1172  35330  bnj1174  35332  bnj1176  35334  bnj1186  35336  bnj1189  35338  bnj1253  35346  bnj1279  35347  bnj1371  35358  bnj1374  35360  bnj1312  35387  exdifsn  35408  axnulALT2  35411  axprALT2  35441  fineqvrep  35446  fineqvpow  35447  axreg  35459  axregscl  35460  axregs  35471  axpowg  35478  onvfowev  35495  lfuhgr3  35507  loop1cycl  35524  satfvsucsuc  35752  satf0op  35764  axextprim  36088  axrepprim  36089  axunprim  36090  axpowprim  36091  axregprim  36092  axinfprim  36093  axacprim  36094  dftr6  36138  coep  36139  coepr  36140  dffr5  36141  cnvco1  36146  cnvco2  36147  eldm3  36148  fundmpss  36154  dfdm5  36160  dfrn5  36161  elima4  36163  axextdfeq  36182  19.12b  36186  axextndbi  36189  brtxp  36265  brpprod  36270  brsset  36274  dfon3  36277  brtxpsd  36279  elfix  36288  dffix2  36290  sscoid  36298  dffun10  36299  elfuns  36300  elsingles  36303  snelsingles  36307  dfiota3  36308  brimg  36322  brapply  36323  brcup  36324  brcap  36325  lemsuccf  36326  funpartlem  36329  brrestrict  36336  dfrecs2  36337  dfrdg4  36338  sumeq2si  36599  prodeq2si  36601  cbvoprab2vw  36635  cbvoprab23vw  36637  cbvprodvw2  36644  neifg  36767  regsfromregtco  36934  regsfromunir1  36936  mh-prprimbi  36939  mh-unprimbi  36940  mh-infprim1bi  36942  mh-infprim2bi  36943  mh-infprim3bi  36944  bj-df-sb  37157  bj-dfsbc  37159  bj-equsexval  37167  bj-eeanvw  37225  bj-substw  37235  eliminable-abelv  37389  eliminable-abelab  37390  bj-denoteslem  37391  bj-rexvw  37400  bj-csbsnlem  37423  bj-gabima  37460  bj-snsetex  37483  bj-elsngl  37488  bj-snglc  37489  bj-abex  37550  bj-clex  37551  bj-clel3gALT  37568  bj-nul  37576  bj-dfid2ALT  37585  bj-rep  37593  bj-axseprep  37594  bj-restpw  37617  bj-restuni  37622  bj-dfmpoa  37643  bj-opabco  37715  bj-xpcossxp  37716  bj-imdirco  37717  mptsnunlem  37867  topdifinffinlem  37876  difunieq  37903  wl-dfclab  38123  poimirlem26  38180  ismblfin  38195  itg2addnclem3  38207  itg2addnc  38208  ismgmOLD  38384  sbcexfi  38651  sbccom2lem  38658  eldmres  38811  ecinn0  38887  ineleq  38888  moantr  38906  dmcnvep  38922  rnxrn  38955  rnxrnres  38956  dmsucmap  39002  dfcoss2  39037  dfcoss3  39038  cosscnv  39040  coss1cnvres  39041  coss2cnvepres  39042  1cossres  39053  cocossss  39060  rncossdmcoss  39079  eldmcoss2  39083  coss0  39103  cossid  39104  dfssr2  39113  eldmqs1cossres  39278  prtlem16  39528  prter2  39540  islshpat  39676  islpln5  40194  islvol5  40238  pmapglb  40429  polval2N  40565  cdlemftr3  41224  dibelval3  41806  dicelval3  41839  dihglb2  42001  sn-axrep5v  42871  prjspeclsp  43229  euabsn2w  43296  diophrex  43391  onsupmaxb  43851  nnoeomeqom  43924  tfsconcatlem  43948  tfsconcat0i  43957  rp-isfinite6  44129  snen1g  44135  relintab  44194  imaiun1  44262  coiun1  44263  clsk3nimkb  44651  expandexn  44884  ismnuprim  44889  rr-groth  44894  ismnushort  44896  rr-grothshortbi  44898  19.36vv  44978  19.37vv  44980  pm11.58  44985  pm11.6  44987  pm13.192  45005  2sbc5g  45011  iotasbc2  45015  onfrALTlem5  45136  onfrALTlem1  45142  ax6e2nd  45152  2sb5nd  45154  en3lplem2VD  45437  onfrALTlem5VD  45478  relopabVD  45494  ax6e2ndVD  45501  2sb5ndVD  45503  ax6e2ndALT  45523  2sb5ndALT  45525  dfac5prim  45584  brpermmodel  45597  permaxrep  45600  permac8prim  45608  rfcnnnub  45641  stoweidlem34  46633  stoweidlem35  46634  stoweidlem60  46659  smfpimcc  47407  ichexmpl1  48100  sprid  48105  dfgric2  48562  usgrgrtrirex  48597  grlimgrtri  48650  eliunxp2  48992  mosssn2  49473  coxp  49489  istermc  50130  setrec1lem3  50345  elpglem3  50369  eximp-surprise  50440