Theorem rexbii 3079

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  ∃wrex 3056

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-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.29imd  3097  r19.43  3100  3r19.43  3101  2rexbii  3108  rexnal2  3114  r19.42v  3164  r19.41vv  3202  3reeanv  3205  cbvrex2vw  3215  rexcom4a  3262  rexcom13  3265  rexrot4  3266  2ex2rexrot  3267  cbvrex2v  3335  rexcom4b  3468  ceqsrex2v  3608  clel5  3615  reu7  3686  2reu5a  3698  0el  4312  n0snor2el  4784  uni0b  4884  iuncom  4949  iuncom4  4950  iuniin  4954  dfiunv2  4984  iunab  5002  iunid  5011  iunsn  5016  iunn0  5017  iunin2  5021  iundif2  5024  iunun  5043  iunxiun  5047  iunpwss  5057  axrep6OLD  5229  inuni  5290  reusv2lem5  5342  iunopab  5502  dffr2  5580  dffr2ALT  5581  frc  5582  frminex  5598  dfepfr  5603  epfrc  5604  xpiundi  5690  xpiundir  5691  reliin  5762  iunxpf  5793  cnvuni  5831  dmiun  5858  dmopab2rex  5862  elres  5974  elidinxp  5998  dfima3  6017  dffr3  6053  rniun  6100  xpdifid  6121  dminxp  6133  imaco  6204  coiun  6210  imaindm  6252  dffr4  6273  frpomin2  6294  sucel  6388  isarep1  6576  rexrn  7026  ralrn  7027  elrnrexdmb  7029  fnasrn  7084  ralima  7177  reximaOLD  7179  ralimaOLD  7180  abrexco  7184  imaiun  7185  fliftcnv  7251  imaeqsexvOLD  7303  rexrnmpo  7492  imaeqexov  7590  iunpw  7710  abrexex2g  7902  el2xptp  7973  poxp2  8079  poxp3  8086  soseq  8095  frrlem9  8230  rdglem1  8340  tz7.49  8370  oarec  8483  omeu  8506  qsid  8711  eroveu  8742  ixp0  8861  fimax2g  9176  marypha2lem2  9326  dfsup2  9334  infcllem  9378  dfoi  9403  wemapsolem  9442  zfregcl  9486  zfregclOLD  9487  zfreg  9488  zfregfr  9500  oemapso  9578  brttrcl2  9610  ttrclresv  9613  zfregs2  9629  infenaleph  9988  isinfcard  9989  kmlem7  10054  kmlem13  10060  fin23lem26  10222  dffin1-5  10285  fin12  10310  numth  10369  ac6n  10382  zorn2lem7  10399  zorng  10401  brdom7disj  10428  brdom6disj  10429  uniwun  10637  axgroth5  10721  axgroth4  10729  grothprim  10731  npomex  10893  genpass  10906  elreal  11028  dfinfre  12109  infrenegsup  12111  uzwo  12815  ublbneg  12837  xrinfmss2  13216  4fvwrd4  13554  fsuppmapnn0fiubex  13905  fsuppmapnn0ub  13908  mptnn0fsuppr  13912  hashge2el2dif  14393  cshwsexa  14737  dfrtrclrec2  14971  rexanuz  15259  rexfiuz  15261  clim0  15419  cbvsum  15608  cbvsumv  15609  incexc2  15751  cbvprod  15826  cbvprodv  15827  prodeq1i  15829  fprodle  15909  iprodmul  15916  divalglem10  16319  divalgb  16321  ncoprmlnprm  16645  pythagtriplem2  16735  pythagtriplem19  16751  pythagtrip  16752  pceu  16764  prmreclem6  16839  4sqlem12  16874  cshwshashlem1  17013  cshwshash  17022  imasaddfnlem  17438  isdrs2  18218  chnfi  18546  smndex1mgm  18821  smndex1n0mnd  18826  pmtrprfvalrn  19406  pgpfac1lem5  19999  dvdsrval  20285  opprunit  20301  lsmspsn  21024  lsmelval2  21025  islpidl  21268  pzriprnglem3  21426  pzriprnglem10  21433  mat1dimelbas  22392  mat1dimbas  22393  mdetunilem8  22540  pmatcollpw2lem  22698  tgval2  22877  ntreq0  22998  isclo2  23009  neiptopnei  23053  ist0-3  23266  tgcmp  23322  cmpfi  23329  is1stc2  23363  unisngl  23448  xkobval  23507  txtube  23561  txcmplem1  23562  xkococnlem  23580  eltsms  24054  metrest  24445  iscau3  25211  bcth  25262  pmltpc  25384  itg2i1fseq  25689  itg2cn  25697  plyun0  26135  aaliou3lem9  26291  1cubr  26785  dchrvmasumlema  27444  selbergsb  27519  ostth  27583  noseponlem  27609  nosepon  27610  nolt02o  27640  noinfbnd1lem1  27668  noinfbnd1lem4  27671  cuteq1  27784  elold  27820  made0  27824  lrrecfr  27892  sleadd1  27938  addsuniflem  27950  addsasslem1  27952  addsasslem2  27953  mulsrid  28058  mulsuniflem  28094  addsdilem1  28096  addsdilem2  28097  mulsasslem1  28108  mulsasslem2  28109  zs12ge0  28399  renegscl  28406  istrkg2ld  28444  tglowdim1i  28485  legtrid  28575  midex  28721  ishpg  28743  brbtwn2  28890  colinearalg  28895  ax5seg  28923  axpasch  28926  axlowdimlem6  28932  axeuclidlem  28947  axeuclid  28948  elntg2  28970  umgr2edg1  29196  umgr2edgneu  29199  nbgrsym  29348  isuvtx  29380  usgr2pth0  29750  wlkiswwlksupgr2  29862  clwwlknun  30099  4cycl2vnunb  30277  fusgreg2wsp  30323  lpni  30467  nmobndseqi  30766  hhcmpl  31187  shne0i  31435  nmcopexi  32014  nmcfnexi  32038  cdj3lem3b  32427  rexcom4f  32454  reuxfrdf  32477  iunin1f  32544  ofpreima  32654  intimafv  32699  fpwrelmapffslem  32722  tosglblem  32962  xrnarchi  33160  isunit2  33214  isdrng4  33268  dvdsrspss  33359  lsmsnorb  33363  lsmsnorb2  33364  1arithufdlem4  33519  constrconj  33765  ordtconnlem1  33944  lmdvg  33973  esumfsup  34090  reprsuc  34635  reprdifc  34647  bnj168  34749  bnj1185  34812  bnj1542  34876  bnj865  34942  bnj916  34952  bnj983  34970  bnj1176  35024  bnj1189  35028  bnj1296  35040  bnj1398  35053  bnj1450  35069  bnj1463  35074  nummin  35111  axregszf  35134  fineqvnttrclse  35151  onvf1odlem1  35154  loop1cycl  35188  cvmliftlem15  35349  cvmlift2lem12  35365  satfvsuclem2  35411  satfvsucsuc  35416  satfdm  35420  satf0  35423  dmopab3rexdif  35456  rexxfr3dALT  35690  dffr5  35805  dfon2lem9  35840  brbigcup  35947  elfuns  35964  brimage  35975  brimg  35986  dfrecs2  36001  imagesset  36004  brub  36005  brsegle  36159  sumeq2si  36253  prodeq2si  36255  cbvprodvw2  36298  filnetlem4  36432  bj-rexcom4bv  36933  bj-rexcom4b  36934  bj-elsngl  37019  bj-rest10  37139  bj-restreg  37150  bj-mpomptALT  37170  nlpineqsn  37459  fvineqsneq  37463  iundif1  37640  matunitlindflem1  37662  poimirlem1  37667  poimirlem30  37696  poimirlem32  37698  poimir  37699  ismblfin  37707  volsupnfl  37711  itg2addnclem3  37719  fdc  37791  isfldidl  38114  eldmqsres2  38332  n0elqs  38370  rnxrncnvepres  38453  rnxrnidres  38454  dfcoels  38538  br1cossinres  38555  br1cossinidres  38557  br1cossincnvepres  38558  br1cossxrnidres  38559  br1cossxrncnvepres  38560  br1cossxrncnvssrres  38606  eldmqs1cossres  38763  disjdmqscossss  38907  prtlem10  38970  prter2  38986  islshpat  39122  lshpsmreu  39214  2dim  39575  islpln5  39640  lplnexatN  39668  islvol5  39684  dalem18  39786  dalem20  39798  lhpexle2  40115  lhpexle3  40117  lhpex2leN  40118  4atex2  40182  4atex2-0bOLDN  40184  cdlemftr3  40670  cdlemg17pq  40777  cdlemg19  40789  cdlemg21  40791  cdlemg33d  40814  dva1dim  41090  dih1dimatlem  41434  dihglb2  41447  dvh2dim  41550  mapdrvallem2  41750  mapdpglem3  41780  hdmapglem7a  42032  hashnexinjle  42228  aks6d1c5  42238  supinf  42341  fimgmcyclem  42632  dffltz  42733  elrfirn  42793  isnacs2  42804  isnacs3  42808  sbc2rex  42885  4rexfrabdioph  42896  eldioph4b  42909  fphpd  42914  fiphp3d  42917  rencldnfilem  42918  rmxdioph  43114  expdiophlem1  43119  islnm2  43176  onmaxnelsup  43321  onsupnmax  43326  onsupuni  43327  onsupmaxb  43337  tfsconcatlem  43434  tfsconcatrn  43440  oadif1lem  43477  oadif1  43478  elimaint  43747  cnviun  43748  imaiun1  43749  coiun1  43750  elintima  43751  briunov2  43780  clsk3nimkb  44138  expandrexn  44389  prmunb2  44409  zfregs2VD  44938  n0abso  45074  sswfaxreg  45085  evth2f  45117  evthf  45129  ndisj2  45153  rexanuz2nf  45595  fnlimabslt  45782  climbddf  45790  limsupub  45807  limsuppnflem  45813  limsupubuz  45816  limsupre2lem  45827  limsupreuz  45840  limsupvaluz2  45841  cnrefiisplem  45932  cnrefiisp  45933  stoweidlem28  46131  fourierdlem63  46272  fourierdlem65  46274  fourierdlem89  46298  fourierdlem90  46299  fourierdlem91  46300  fourierdlem100  46309  sge0pnfmpt  46548  ovn0  46669  smfaddlem1  46866  smflimlem4  46877  fsetsniunop  47154  2rexsb  47206  2rexrsb  47207  cbvrex2  47209  2reu8i  47218  clnbgrsym  47943  isubgr3stgrlem6  48076  copisnmnd  48274  pgrpgt2nabl  48471  islindeps  48559  lindslinindsimp1  48563  lindslinindsimp2  48569  islindeps2  48589  islininds2  48590  isldepslvec2  48591  ldepslinc  48615  sepnsepolem1  49027