Theorem rexbii 3109

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Dec-2019.)

Hypothesis

Ref	Expression
rexbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rexbii	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rexbiia 3107	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.29imd  3127  r19.43  3130  3r19.43  3131  2rexbii  3138  rexnal2  3144  r19.42v  3194  r19.41vv  3232  3reeanv  3235  cbvrex2vw  3245  rexcom4a  3292  rexcom13  3295  rexrot4  3296  2ex2rexrot  3297  cbvrex2v  3354  rexcom4b  3481  ceqsrex2v  3611  clel5  3618  reu7  3689  2reu5a  3701  0el  4310  n0snor2el  4787  uni0b  4893  iuncom  4958  iuncom4  4959  iuniin  4963  dfiunv2  4991  iunab  5009  iunid  5018  iunsn  5023  iunn0  5024  iunin2  5028  iundif2  5031  iunun  5052  iunxiun  5056  iunpwss  5066  inuni  5310  reusv2lem5  5363  iunopab  5533  dffr2  5611  dffr2ALT  5612  frc  5613  frminex  5629  dfepfr  5634  epfrc  5635  xpiundi  5721  xpiundir  5722  reliin  5794  el2xptp  5819  iunxpf  5825  cnvuni  5867  dmiun  5894  dmopab2rex  5898  elres  6008  elidinxp  6035  dfima3  6058  dffr3  6096  rniun  6138  xpdifid  6158  xpdifcnvepel  6159  dminxp  6171  imaco  6252  coiun  6258  imaindm  6302  dffr4  6323  frpomin2  6344  sucel  6439  isarep1  6629  rexrn  7088  ralrn  7089  elrnrexdmb  7091  fnasrn  7149  ralima  7244  abrexco  7249  imaiun  7250  fliftcnv  7320  rexrnmpo  7561  imaeqexov  7660  mpt3mpt  7686  iunpw  7786  abrexex2g  7977  poxp2  8163  poxp3  8170  soseq  8179  frrlem9  8316  rdglem1  8427  tz7.49  8459  oarec  8574  omeu  8597  qsid  8806  eroveu  8837  ixp0  8963  fimax2g  9281  marypha2lem2  9432  dfsup2  9440  infcllem  9484  dfoi  9509  wemapsolem  9548  zfregcl  9592  zfregclOLD  9593  zfreg  9594  zfregfr  9609  oemapso  9687  brttrcl2  9719  ttrclresv  9722  zfregs2  9738  infenaleph  10174  isinfcard  10175  kmlem7  10239  kmlem13  10245  fin23lem26  10407  dffin1-5  10470  fin12  10495  numth  10554  ac6n  10567  zorn2lem7  10584  zorng  10586  brdom7disj  10614  brdom6disj  10615  uniwun  10829  axgroth5  10913  axgroth4  10921  grothprim  10923  npomex  11085  genpass  11098  elreal  11220  dfinfre  12302  infrenegsup  12304  uzwo  13042  ublbneg  13064  xrinfmss2  13445  4fvwrd4  13786  fsuppmapnn0fiubex  14139  fsuppmapnn0ub  14142  mptnn0fsuppr  14146  hashge2el2dif  14629  cshwsexa  14980  dfrtrclrec2  15217  rexanuz  15519  rexfiuz  15521  clim0  15679  cbvsum  15868  cbvsumv  15869  incexc2  16013  cbvprod  16088  cbvprodv  16089  prodeq1i  16091  fprodle  16169  iprodmul  16176  divalglem10  16578  divalgb  16580  ncoprmlnprm  16910  pythagtriplem2  17001  pythagtriplem19  17017  pythagtrip  17018  pceu  17030  prmreclem6  17105  4sqlem12  17140  cshwshashlem1  17279  cshwshash  17288  imasaddfnlem  17706  isdrs2  18486  chnfi  18814  smndex1mgm  19112  smndex1n0mnd  19117  pmtrprfvalrn  19708  pgpfac1lem5  20301  dvdsrval  20597  opprunit  20613  isdrng4  20998  isdrng3lem1  21011  lsmspsn  21365  lsmelval2  21366  islpidl  21655  pzriprnglem3  21795  pzriprnglem10  21802  mat1dimelbas  22792  mat1dimbas  22793  mdetunilem8  22940  matunitlindflem1  23000  pmatcollpw2lem  23101  tgval2  23280  ntreq0  23401  isclo2  23412  neiptopnei  23456  ist0-3  23669  tgcmp  23725  cmpfi  23732  is1stc2  23766  unisngl  23852  xkobval  23911  txtube  23965  txcmplem1  23966  xkococnlem  23984  eltsms  24458  metrest  24849  iscau3  25605  bcth  25656  pmltpc  25777  itg2i1fseq  26082  itg2cn  26090  plyun0  26521  plyconz  26637  aaliou3lem9  26683  1cubr  27176  dchrvmasumlema  27833  selbergsb  27908  ostth  27972  noseponlem  28027  nosepon  28028  nolt02o  28058  noinfbnd1lem1  28086  noinfbnd1lem4  28089  cuteq1  28209  elold  28251  made0  28255  lrrecfr  28335  leadds1  28381  addsuniflem  28393  addsasslem1  28395  addsasslem2  28396  mulsrid  28505  mulsuniflem  28541  addsdilem1  28543  addsdilem2  28544  mulsasslem1  28555  mulsasslem2  28556  z12sge0  28875  elreno2  28887  renegscl  28890  istrkg2ld  28928  tglowdim1i  28970  legtrid  29060  midex  29219  ishpg  29243  brbtwn2  29489  colinearalg  29494  ax5seg  29522  axpasch  29525  axlowdimlem6  29531  axeuclidlem  29546  axeuclid  29547  elntg2  29569  umgr2edg1  29798  umgr2edgneu  29801  nbgrsym  29950  isuvtx  29982  usgr2pth0  30357  wlkiswwlksupgr2  30472  clwwlknun  30709  loop1cycl  30750  4cycl2vnunb  30897  fusgreg2wsp  30943  lpni  31088  nmobndseqi  31387  hhcmpl  31808  shne0i  32056  nmcopexi  32635  nmcfnexi  32659  cdj3lem3b  33048  rexcom4f  33113  reuxfrdf  33135  iunin1f  33200  ofpreima  33307  intimafv  33352  fpwrelmapffslem  33371  tosglblem  33582  xrnarchi  33792  isunit2  33847  dvdsrspss  33989  lsmsnorb  33993  lsmsnorb2  33994  1arithufdlem4  34126  constrconj  34424  ordtconnlem1  34603  lmdvg  34632  esumfsup  34749  reprsuc  35291  reprdifc  35303  bnj168  35408  bnj1185  35470  bnj1542  35534  bnj865  35600  bnj916  35610  bnj983  35628  bnj1176  35682  bnj1189  35686  bnj1296  35698  bnj1398  35711  bnj1450  35727  bnj1463  35732  nummin  35775  fineqvnttrclse  35849  axregszf  35854  onvf1odlem1  35951  cvmliftlem15  36150  cvmlift2lem12  36166  satfvsuclem2  36212  satfvsucsuc  36217  satfdm  36221  satf0  36224  dmopab3rexdif  36257  rexxfr3dALT  36491  dffr5  36612  dfon2lem9  36646  brbigcup  36753  elfuns  36770  brimage  36781  brimg  36792  dfrecs2  36807  imagesset  36810  brub  36811  dffr7  36813  brsegle  36966  sumeq2si  37084  prodeq2si  37086  cbvprodvw2  37129  filnetlem4  37262  bj-rexcom4bv  37887  bj-rexcom4b  37888  bj-elsngl  37974  bj-axseprep  38083  bj-rest10  38102  bj-restreg  38113  bj-mpomptALT  38134  nlpineqsn  38425  fvineqsneq  38429  iundif1  38616  poimirlem1  38633  poimirlem30  38662  poimirlem32  38664  poimir  38665  ismblfin  38673  volsupnfl  38677  itg2addnclem3  38685  dfproplem  38735  fdc  38773  isfldidl  39096  eldmqsres2  39320  n0elqs  39358  rnxrncnvepres  39449  rnxrnidres  39450  dfcoels  39546  br1cossinres  39563  br1cossinidres  39565  br1cossincnvepres  39566  br1cossxrnidres  39567  br1cossxrncnvepres  39568  br1cossxrncnvssrres  39614  eldmqs1cossres  39770  disjdmqscossss  39932  prtlem10  40016  prter2  40032  islshpat  40168  lshpsmreu  40260  2dim  40621  islpln5  40686  lplnexatN  40714  islvol5  40730  dalem18  40832  dalem20  40844  lhpexle2  41161  lhpexle3  41163  lhpex2leN  41164  4atex2  41228  4atex2-0bOLDN  41230  cdlemftr3  41716  cdlemg17pq  41823  cdlemg19  41835  cdlemg21  41837  cdlemg33d  41860  dva1dim  42136  dih1dimatlem  42480  dihglb2  42493  dvh2dim  42596  mapdrvallem2  42796  mapdpglem3  42826  hdmapglem7a  43078  hashnexinjle  43273  aks6d1c5  43283  supinf  43387  fimgmcyclem  43691  dffltz  43764  elrfirn  43800  isnacs2  43811  isnacs3  43815  sbc2rex  43890  4rexfrabdioph  43899  eldioph4b  43912  fphpd  43917  fiphp3d  43920  rencldnfilem  43921  rmxdioph  44117  expdiophlem1  44122  islnm2  44174  onmaxnelsup  44319  onsupnmax  44324  onsupuni  44325  onsupmaxb  44335  tfsconcatlem  44432  tfsconcatrn  44438  oadif1lem  44475  oadif1  44476  elimaint  44743  cnviun  44744  imaiun1  44745  coiun1  44746  elintima  44747  briunov2  44776  clsk3nimkb  45134  expandrexn  45369  prmunb2  45389  zfregs2VD  45917  n0abso  46060  sswfaxreg  46071  evth2f  46126  evthf  46138  ndisj2  46162  rexanuz2nf  46596  fnlimabslt  46783  climbddf  46791  limsupub  46808  limsuppnflem  46814  limsupubuz  46817  limsupre2lem  46828  limsupreuz  46841  limsupvaluz2  46842  cnrefiisplem  46933  cnrefiisp  46934  stoweidlem28  47132  fourierdlem63  47273  fourierdlem65  47275  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem100  47310  sge0pnfmpt  47549  ovn0  47670  smfaddlem1  47867  smflimlem4  47878  fsetsniunop  48213  2rexsb  48265  2rexrsb  48266  cbvrex2  48268  2reu8i  48277  clnbgrsym  49030  isubgr3stgrlem6  49163  copisnmnd  49360  pgrpgt2nabl  49572  islindeps  49659  lindslinindsimp1  49663  lindslinindsimp2  49669  islindeps2  49689  islininds2  49690  isldepslvec2  49691  ldepslinc  49715  sepnsepolem1  50130  ralsbii  51066