Theorem rexbii 3084

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  r19.29imd  3102  r19.43  3105  3r19.43  3106  2rexbii  3113  rexnal2  3119  r19.42v  3169  r19.41vv  3207  3reeanv  3210  cbvrex2vw  3220  rexcom4a  3267  rexcom13  3270  rexrot4  3271  2ex2rexrot  3272  cbvrex2v  3331  rexcom4b  3461  ceqsrex2v  3600  clel5  3607  reu7  3678  2reu5a  3690  0el  4303  n0snor2el  4776  uni0b  4876  iuncom  4941  iuncom4  4942  iuniin  4946  dfiunv2  4976  iunab  4994  iunid  5003  iunsn  5008  iunn0  5009  iunin2  5013  iundif2  5016  iunun  5035  iunxiun  5039  iunpwss  5049  axrep6OLD  5222  inuni  5291  reusv2lem5  5344  iunopab  5514  dffr2  5592  dffr2ALT  5593  frc  5594  frminex  5610  dfepfr  5615  epfrc  5616  xpiundi  5702  xpiundir  5703  reliin  5773  iunxpf  5803  cnvuni  5841  dmiun  5868  dmopab2rex  5872  elres  5985  elidinxp  6009  dfima3  6028  dffr3  6064  rniun  6111  xpdifid  6132  dminxp  6144  imaco  6215  coiun  6221  imaindm  6263  dffr4  6284  frpomin2  6305  sucel  6399  isarep1  6587  rexrn  7039  ralrn  7040  elrnrexdmb  7042  fnasrn  7098  ralima  7192  reximaOLD  7194  ralimaOLD  7195  abrexco  7199  imaiun  7200  fliftcnv  7266  imaeqsexvOLD  7318  rexrnmpo  7507  imaeqexov  7605  iunpw  7725  abrexex2g  7917  el2xptp  7988  poxp2  8093  poxp3  8100  soseq  8109  frrlem9  8244  rdglem1  8354  tz7.49  8384  oarec  8497  omeu  8520  qsid  8728  eroveu  8759  ixp0  8879  fimax2g  9196  marypha2lem2  9349  dfsup2  9357  infcllem  9401  dfoi  9426  wemapsolem  9465  zfregcl  9509  zfregclOLD  9510  zfreg  9511  zfregfr  9525  oemapso  9603  brttrcl2  9635  ttrclresv  9638  zfregs2  9654  infenaleph  10013  isinfcard  10014  kmlem7  10079  kmlem13  10085  fin23lem26  10247  dffin1-5  10310  fin12  10335  numth  10394  ac6n  10407  zorn2lem7  10424  zorng  10426  brdom7disj  10453  brdom6disj  10454  uniwun  10663  axgroth5  10747  axgroth4  10755  grothprim  10757  npomex  10919  genpass  10932  elreal  11054  dfinfre  12137  infrenegsup  12139  uzwo  12861  ublbneg  12883  xrinfmss2  13263  4fvwrd4  13602  fsuppmapnn0fiubex  13954  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  hashge2el2dif  14442  cshwsexa  14786  dfrtrclrec2  15020  rexanuz  15308  rexfiuz  15310  clim0  15468  cbvsum  15657  cbvsumv  15658  incexc2  15803  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  fprodle  15961  iprodmul  15968  divalglem10  16371  divalgb  16373  ncoprmlnprm  16698  pythagtriplem2  16788  pythagtriplem19  16804  pythagtrip  16805  pceu  16817  prmreclem6  16892  4sqlem12  16927  cshwshashlem1  17066  cshwshash  17075  imasaddfnlem  17492  isdrs2  18272  chnfi  18600  smndex1mgm  18878  smndex1n0mnd  18883  pmtrprfvalrn  19463  pgpfac1lem5  20056  dvdsrval  20341  opprunit  20357  lsmspsn  21079  lsmelval2  21080  islpidl  21323  pzriprnglem3  21463  pzriprnglem10  21470  mat1dimelbas  22436  mat1dimbas  22437  mdetunilem8  22584  pmatcollpw2lem  22742  tgval2  22921  ntreq0  23042  isclo2  23053  neiptopnei  23097  ist0-3  23310  tgcmp  23366  cmpfi  23373  is1stc2  23407  unisngl  23492  xkobval  23551  txtube  23605  txcmplem1  23606  xkococnlem  23624  eltsms  24098  metrest  24489  iscau3  25245  bcth  25296  pmltpc  25417  itg2i1fseq  25722  itg2cn  25730  plyun0  26162  aaliou3lem9  26316  1cubr  26806  dchrvmasumlema  27463  selbergsb  27538  ostth  27602  noseponlem  27628  nosepon  27629  nolt02o  27659  noinfbnd1lem1  27687  noinfbnd1lem4  27690  cuteq1  27809  elold  27851  made0  27855  lrrecfr  27935  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  mulsrid  28105  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  z12sge0  28475  elreno2  28487  renegscl  28490  istrkg2ld  28528  tglowdim1i  28569  legtrid  28659  midex  28805  ishpg  28827  brbtwn2  28974  colinearalg  28979  ax5seg  29007  axpasch  29010  axlowdimlem6  29016  axeuclidlem  29031  axeuclid  29032  elntg2  29054  umgr2edg1  29280  umgr2edgneu  29283  nbgrsym  29432  isuvtx  29464  usgr2pth0  29833  wlkiswwlksupgr2  29945  clwwlknun  30182  4cycl2vnunb  30360  fusgreg2wsp  30406  lpni  30551  nmobndseqi  30850  hhcmpl  31271  shne0i  31519  nmcopexi  32098  nmcfnexi  32122  cdj3lem3b  32511  rexcom4f  32537  reuxfrdf  32560  iunin1f  32627  ofpreima  32738  intimafv  32784  fpwrelmapffslem  32805  tosglblem  33034  xrnarchi  33245  isunit2  33301  isdrng4  33356  dvdsrspss  33447  lsmsnorb  33451  lsmsnorb2  33452  1arithufdlem4  33607  constrconj  33889  ordtconnlem1  34068  lmdvg  34097  esumfsup  34214  reprsuc  34759  reprdifc  34771  bnj168  34873  bnj1185  34935  bnj1542  34999  bnj865  35065  bnj916  35075  bnj983  35093  bnj1176  35147  bnj1189  35151  bnj1296  35163  bnj1398  35176  bnj1450  35192  bnj1463  35197  nummin  35236  fineqvnttrclse  35268  axregszf  35273  onvf1odlem1  35285  loop1cycl  35319  cvmliftlem15  35480  cvmlift2lem12  35496  satfvsuclem2  35542  satfvsucsuc  35547  satfdm  35551  satf0  35554  dmopab3rexdif  35587  rexxfr3dALT  35821  dffr5  35936  dfon2lem9  35971  brbigcup  36078  elfuns  36095  brimage  36106  brimg  36117  dfrecs2  36132  imagesset  36135  brub  36136  brsegle  36290  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  filnetlem4  36563  bj-rexcom4bv  37189  bj-rexcom4b  37190  bj-elsngl  37275  bj-axseprep  37381  bj-rest10  37400  bj-restreg  37411  bj-mpomptALT  37431  nlpineqsn  37724  fvineqsneq  37728  iundif1  37915  matunitlindflem1  37937  poimirlem1  37942  poimirlem30  37971  poimirlem32  37973  poimir  37974  ismblfin  37982  volsupnfl  37986  itg2addnclem3  37994  fdc  38066  isfldidl  38389  eldmqsres2  38615  n0elqs  38653  rnxrncnvepres  38744  rnxrnidres  38745  dfcoels  38841  br1cossinres  38858  br1cossinidres  38860  br1cossincnvepres  38861  br1cossxrnidres  38862  br1cossxrncnvepres  38863  br1cossxrncnvssrres  38909  eldmqs1cossres  39065  disjdmqscossss  39227  prtlem10  39311  prter2  39327  islshpat  39463  lshpsmreu  39555  2dim  39916  islpln5  39981  lplnexatN  40009  islvol5  40025  dalem18  40127  dalem20  40139  lhpexle2  40456  lhpexle3  40458  lhpex2leN  40459  4atex2  40523  4atex2-0bOLDN  40525  cdlemftr3  41011  cdlemg17pq  41118  cdlemg19  41130  cdlemg21  41132  cdlemg33d  41155  dva1dim  41431  dih1dimatlem  41775  dihglb2  41788  dvh2dim  41891  mapdrvallem2  42091  mapdpglem3  42121  hdmapglem7a  42373  hashnexinjle  42568  aks6d1c5  42578  supinf  42681  fimgmcyclem  42978  dffltz  43067  elrfirn  43127  isnacs2  43138  isnacs3  43142  sbc2rex  43217  4rexfrabdioph  43226  eldioph4b  43239  fphpd  43244  fiphp3d  43247  rencldnfilem  43248  rmxdioph  43444  expdiophlem1  43449  islnm2  43506  onmaxnelsup  43651  onsupnmax  43656  onsupuni  43657  onsupmaxb  43667  tfsconcatlem  43764  tfsconcatrn  43770  oadif1lem  43807  oadif1  43808  elimaint  44076  cnviun  44077  imaiun1  44078  coiun1  44079  elintima  44080  briunov2  44109  clsk3nimkb  44467  expandrexn  44718  prmunb2  44738  zfregs2VD  45267  n0abso  45403  sswfaxreg  45414  evth2f  45446  evthf  45458  ndisj2  45482  rexanuz2nf  45920  fnlimabslt  46107  climbddf  46115  limsupub  46132  limsuppnflem  46138  limsupubuz  46141  limsupre2lem  46152  limsupreuz  46165  limsupvaluz2  46166  cnrefiisplem  46257  cnrefiisp  46258  stoweidlem28  46456  fourierdlem63  46597  fourierdlem65  46599  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem100  46634  sge0pnfmpt  46873  ovn0  46994  smfaddlem1  47191  smflimlem4  47202  fsetsniunop  47497  2rexsb  47549  2rexrsb  47550  cbvrex2  47552  2reu8i  47561  clnbgrsym  48314  isubgr3stgrlem6  48447  copisnmnd  48645  pgrpgt2nabl  48842  islindeps  48929  lindslinindsimp1  48933  lindslinindsimp2  48939  islindeps2  48959  islininds2  48960  isldepslvec2  48961  ldepslinc  48985  sepnsepolem1  49397