Theorem rexbii 3112

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 3110	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 209   ∈ wcel 2145  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  r19.29imd  3130  r19.43  3133  3r19.43  3134  2rexbii  3141  rexnal2  3147  r19.42v  3197  r19.41vv  3235  3reeanv  3238  cbvrex2vw  3248  rexcom4a  3295  rexcom13  3298  rexrot4  3299  2ex2rexrot  3300  cbvrex2v  3359  rexcom4b  3488  ceqsrex2v  3620  clel5  3627  reu7  3698  2reu5a  3710  0el  4319  n0snor2el  4793  uni0b  4894  iuncom  4959  iuncom4  4960  iuniin  4964  dfiunv2  4993  iunab  5011  iunid  5020  iunsn  5025  iunn0  5026  iunin2  5030  iundif2  5033  iunun  5054  iunxiun  5058  iunpwss  5068  axrep6OLD  5241  inuni  5310  reusv2lem5  5363  iunopab  5534  dffr2  5612  dffr2ALT  5613  frc  5614  frminex  5630  dfepfr  5635  epfrc  5636  xpiundi  5722  xpiundir  5723  reliin  5794  iunxpf  5824  cnvuni  5866  dmiun  5893  dmopab2rex  5897  elres  6009  elidinxp  6036  dfima3  6055  dffr3  6091  rniun  6135  xpdifid  6156  xpdifcnvepel  6157  dminxp  6169  imaco  6241  coiun  6247  imaindm  6289  dffr4  6310  frpomin2  6331  sucel  6426  isarep1  6614  rexrn  7072  ralrn  7073  elrnrexdmb  7075  fnasrn  7131  ralima  7225  reximaOLD  7227  ralimaOLD  7228  abrexco  7232  imaiun  7233  fliftcnv  7299  imaeqsexvOLD  7351  rexrnmpo  7540  imaeqexov  7638  iunpw  7758  abrexex2g  7949  el2xptp  8020  poxp2  8127  poxp3  8134  soseq  8143  frrlem9  8279  rdglem1  8390  tz7.49  8420  oarec  8535  omeu  8558  qsid  8767  eroveu  8798  ixp0  8917  fimax2g  9234  marypha2lem2  9384  dfsup2  9392  infcllem  9436  dfoi  9461  wemapsolem  9500  zfregcl  9544  zfregclOLD  9545  zfreg  9546  zfregfr  9561  oemapso  9639  brttrcl2  9671  ttrclresv  9674  zfregs2  9690  infenaleph  10063  isinfcard  10064  kmlem7  10128  kmlem13  10134  fin23lem26  10297  dffin1-5  10360  fin12  10385  numth  10444  ac6n  10457  zorn2lem7  10474  zorng  10476  brdom7disj  10503  brdom6disj  10504  uniwun  10713  axgroth5  10797  axgroth4  10805  grothprim  10807  npomex  10969  genpass  10982  elreal  11104  dfinfre  12184  infrenegsup  12186  uzwo  12923  ublbneg  12945  xrinfmss2  13325  4fvwrd4  13664  fsuppmapnn0fiubex  14016  fsuppmapnn0ub  14019  mptnn0fsuppr  14023  hashge2el2dif  14505  cshwsexa  14849  dfrtrclrec2  15083  rexanuz  15385  rexfiuz  15387  clim0  15545  cbvsum  15734  cbvsumv  15735  incexc2  15880  cbvprod  15955  cbvprodv  15956  prodeq1i  15958  fprodle  16038  iprodmul  16045  divalglem10  16448  divalgb  16450  ncoprmlnprm  16775  pythagtriplem2  16865  pythagtriplem19  16881  pythagtrip  16882  pceu  16894  prmreclem6  16969  4sqlem12  17004  cshwshashlem1  17143  cshwshash  17152  imasaddfnlem  17570  isdrs2  18350  chnfi  18678  smndex1mgm  18957  smndex1n0mnd  18962  pmtrprfvalrn  19546  pgpfac1lem5  20139  dvdsrval  20431  opprunit  20447  lsmspsn  21171  lsmelval2  21172  islpidl  21450  pzriprnglem3  21590  pzriprnglem10  21597  mat1dimelbas  22585  mat1dimbas  22586  mdetunilem8  22733  pmatcollpw2lem  22891  tgval2  23070  ntreq0  23191  isclo2  23202  neiptopnei  23246  ist0-3  23459  tgcmp  23515  cmpfi  23522  is1stc2  23556  unisngl  23641  xkobval  23700  txtube  23754  txcmplem1  23755  xkococnlem  23773  eltsms  24247  metrest  24638  iscau3  25394  bcth  25445  pmltpc  25566  itg2i1fseq  25871  itg2cn  25879  plyun0  26311  aaliou3lem9  26468  1cubr  26961  dchrvmasumlema  27618  selbergsb  27693  ostth  27757  noseponlem  27782  nosepon  27783  nolt02o  27813  noinfbnd1lem1  27841  noinfbnd1lem4  27844  cuteq1  27964  elold  28006  made0  28010  lrrecfr  28090  leadds1  28136  addsuniflem  28148  addsasslem1  28150  addsasslem2  28151  mulsrid  28260  mulsuniflem  28296  addsdilem1  28298  addsdilem2  28299  mulsasslem1  28310  mulsasslem2  28311  z12sge0  28630  elreno2  28642  renegscl  28645  istrkg2ld  28683  tglowdim1i  28724  legtrid  28814  midex  28964  ishpg  28986  brbtwn2  29160  colinearalg  29165  ax5seg  29193  axpasch  29196  axlowdimlem6  29202  axeuclidlem  29217  axeuclid  29218  elntg2  29240  umgr2edg1  29466  umgr2edgneu  29469  nbgrsym  29618  isuvtx  29650  usgr2pth0  30019  wlkiswwlksupgr2  30131  clwwlknun  30368  4cycl2vnunb  30546  fusgreg2wsp  30592  lpni  30737  nmobndseqi  31036  hhcmpl  31457  shne0i  31705  nmcopexi  32284  nmcfnexi  32308  cdj3lem3b  32697  rexcom4f  32721  reuxfrdf  32743  iunin1f  32808  ofpreima  32918  intimafv  32964  fpwrelmapffslem  32985  tosglblem  33202  xrnarchi  33412  isunit2  33467  isdrng4  33526  dvdsrspss  33611  lsmsnorb  33615  lsmsnorb2  33616  1arithufdlem4  33749  constrconj  34047  ordtconnlem1  34226  lmdvg  34255  esumfsup  34372  reprsuc  34914  reprdifc  34926  bnj168  35031  bnj1185  35093  bnj1542  35157  bnj865  35223  bnj916  35233  bnj983  35251  bnj1176  35305  bnj1189  35309  bnj1296  35321  bnj1398  35334  bnj1450  35350  bnj1463  35355  nummin  35394  fineqvnttrclse  35427  axregszf  35432  onvf1odlem1  35453  loop1cycl  35495  cvmliftlem15  35656  cvmlift2lem12  35672  satfvsuclem2  35718  satfvsucsuc  35723  satfdm  35727  satf0  35730  dmopab3rexdif  35763  rexxfr3dALT  35997  dffr5  36112  dfon2lem9  36147  brbigcup  36254  elfuns  36271  brimage  36282  brimg  36293  dfrecs2  36308  imagesset  36311  brub  36312  brsegle  36466  sumeq2si  36570  prodeq2si  36572  cbvprodvw2  36615  filnetlem4  36749  bj-rexcom4bv  37374  bj-rexcom4b  37375  bj-elsngl  37460  bj-axseprep  37566  bj-rest10  37585  bj-restreg  37596  bj-mpomptALT  37616  nlpineqsn  37909  fvineqsneq  37913  iundif1  38100  matunitlindflem1  38122  poimirlem1  38127  poimirlem30  38156  poimirlem32  38158  poimir  38159  ismblfin  38167  volsupnfl  38171  itg2addnclem3  38179  fdc  38251  isfldidl  38574  eldmqsres2  38800  n0elqs  38838  rnxrncnvepres  38929  rnxrnidres  38930  dfcoels  39026  br1cossinres  39043  br1cossinidres  39045  br1cossincnvepres  39046  br1cossxrnidres  39047  br1cossxrncnvepres  39048  br1cossxrncnvssrres  39094  eldmqs1cossres  39250  disjdmqscossss  39412  prtlem10  39496  prter2  39512  islshpat  39648  lshpsmreu  39740  2dim  40101  islpln5  40166  lplnexatN  40194  islvol5  40210  dalem18  40312  dalem20  40324  lhpexle2  40641  lhpexle3  40643  lhpex2leN  40644  4atex2  40708  4atex2-0bOLDN  40710  cdlemftr3  41196  cdlemg17pq  41303  cdlemg19  41315  cdlemg21  41317  cdlemg33d  41340  dva1dim  41616  dih1dimatlem  41960  dihglb2  41973  dvh2dim  42076  mapdrvallem2  42276  mapdpglem3  42306  hdmapglem7a  42558  hashnexinjle  42753  aks6d1c5  42763  supinf  42865  fimgmcyclem  43158  dffltz  43223  elrfirn  43283  isnacs2  43294  isnacs3  43298  sbc2rex  43373  4rexfrabdioph  43382  eldioph4b  43395  fphpd  43400  fiphp3d  43403  rencldnfilem  43404  rmxdioph  43600  expdiophlem1  43605  islnm2  43662  onmaxnelsup  43807  onsupnmax  43812  onsupuni  43813  onsupmaxb  43823  tfsconcatlem  43920  tfsconcatrn  43926  oadif1lem  43963  oadif1  43964  elimaint  44232  cnviun  44233  imaiun1  44234  coiun1  44235  elintima  44236  briunov2  44265  clsk3nimkb  44623  expandrexn  44860  prmunb2  44880  zfregs2VD  45408  n0abso  45544  sswfaxreg  45555  evth2f  45594  evthf  45606  ndisj2  45630  rexanuz2nf  46065  fnlimabslt  46252  climbddf  46260  limsupub  46277  limsuppnflem  46283  limsupubuz  46286  limsupre2lem  46297  limsupreuz  46310  limsupvaluz2  46311  cnrefiisplem  46402  cnrefiisp  46403  stoweidlem28  46601  fourierdlem63  46742  fourierdlem65  46744  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem100  46779  sge0pnfmpt  47018  ovn0  47139  smfaddlem1  47336  smflimlem4  47347  fsetsniunop  47642  2rexsb  47694  2rexrsb  47695  cbvrex2  47697  2reu8i  47706  clnbgrsym  48459  isubgr3stgrlem6  48592  copisnmnd  48790  pgrpgt2nabl  48998  islindeps  49085  lindslinindsimp1  49089  lindslinindsimp2  49095  islindeps2  49115  islininds2  49116  isldepslvec2  49117  ldepslinc  49141  sepnsepolem1  49552