Theorem rexbii 3080

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∃wrex 3057

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 3058

This theorem is referenced by:  r19.29imd  3098  r19.43  3101  3r19.43  3102  2rexbii  3109  rexnal2  3115  r19.42v  3165  r19.41vv  3203  3reeanv  3206  cbvrex2vw  3216  rexcom4a  3263  rexcom13  3266  rexrot4  3267  2ex2rexrot  3268  cbvrex2v  3336  rexcom4b  3469  ceqsrex2v  3609  clel5  3616  reu7  3687  2reu5a  3699  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  5761  iunxpf  5792  cnvuni  5830  dmiun  5857  dmopab2rex  5861  elres  5973  elidinxp  5997  dfima3  6016  dffr3  6052  rniun  6099  xpdifid  6120  dminxp  6132  imaco  6203  coiun  6209  imaindm  6251  dffr4  6272  frpomin2  6293  sucel  6387  isarep1  6575  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  9177  marypha2lem2  9327  dfsup2  9335  infcllem  9379  dfoi  9404  wemapsolem  9443  zfregcl  9487  zfregclOLD  9488  zfreg  9489  zfregfr  9501  oemapso  9579  brttrcl2  9611  ttrclresv  9614  zfregs2  9630  infenaleph  9989  isinfcard  9990  kmlem7  10055  kmlem13  10061  fin23lem26  10223  dffin1-5  10286  fin12  10311  numth  10370  ac6n  10383  zorn2lem7  10400  zorng  10402  brdom7disj  10429  brdom6disj  10430  uniwun  10638  axgroth5  10722  axgroth4  10730  grothprim  10732  npomex  10894  genpass  10907  elreal  11029  dfinfre  12110  infrenegsup  12112  uzwo  12811  ublbneg  12833  xrinfmss2  13212  4fvwrd4  13550  fsuppmapnn0fiubex  13901  fsuppmapnn0ub  13904  mptnn0fsuppr  13908  hashge2el2dif  14389  cshwsexa  14733  dfrtrclrec2  14967  rexanuz  15255  rexfiuz  15257  clim0  15415  cbvsum  15604  cbvsumv  15605  incexc2  15747  cbvprod  15822  cbvprodv  15823  prodeq1i  15825  fprodle  15905  iprodmul  15912  divalglem10  16315  divalgb  16317  ncoprmlnprm  16641  pythagtriplem2  16731  pythagtriplem19  16747  pythagtrip  16748  pceu  16760  prmreclem6  16835  4sqlem12  16870  cshwshashlem1  17009  cshwshash  17018  imasaddfnlem  17434  isdrs2  18214  chnfi  18542  smndex1mgm  18817  smndex1n0mnd  18822  pmtrprfvalrn  19402  pgpfac1lem5  19995  dvdsrval  20281  opprunit  20297  lsmspsn  21020  lsmelval2  21021  islpidl  21264  pzriprnglem3  21422  pzriprnglem10  21429  mat1dimelbas  22387  mat1dimbas  22388  mdetunilem8  22535  pmatcollpw2lem  22693  tgval2  22872  ntreq0  22993  isclo2  23004  neiptopnei  23048  ist0-3  23261  tgcmp  23317  cmpfi  23324  is1stc2  23358  unisngl  23443  xkobval  23502  txtube  23556  txcmplem1  23557  xkococnlem  23575  eltsms  24049  metrest  24440  iscau3  25206  bcth  25257  pmltpc  25379  itg2i1fseq  25684  itg2cn  25692  plyun0  26130  aaliou3lem9  26286  1cubr  26780  dchrvmasumlema  27439  selbergsb  27514  ostth  27578  noseponlem  27604  nosepon  27605  nolt02o  27635  noinfbnd1lem1  27663  noinfbnd1lem4  27666  cuteq1  27779  elold  27815  made0  27819  lrrecfr  27887  sleadd1  27933  addsuniflem  27945  addsasslem1  27947  addsasslem2  27948  mulsrid  28053  mulsuniflem  28089  addsdilem1  28091  addsdilem2  28092  mulsasslem1  28103  mulsasslem2  28104  zs12ge0  28394  renegscl  28401  istrkg2ld  28439  tglowdim1i  28480  legtrid  28570  midex  28716  ishpg  28738  brbtwn2  28885  colinearalg  28890  ax5seg  28918  axpasch  28921  axlowdimlem6  28927  axeuclidlem  28942  axeuclid  28943  elntg2  28965  umgr2edg1  29191  umgr2edgneu  29194  nbgrsym  29343  isuvtx  29375  usgr2pth0  29745  wlkiswwlksupgr2  29857  clwwlknun  30094  4cycl2vnunb  30272  fusgreg2wsp  30318  lpni  30462  nmobndseqi  30761  hhcmpl  31182  shne0i  31430  nmcopexi  32009  nmcfnexi  32033  cdj3lem3b  32422  rexcom4f  32449  reuxfrdf  32472  iunin1f  32539  ofpreima  32649  intimafv  32696  fpwrelmapffslem  32719  tosglblem  32962  xrnarchi  33160  isunit2  33214  isdrng4  33268  dvdsrspss  33359  lsmsnorb  33363  lsmsnorb2  33364  1arithufdlem4  33519  constrconj  33779  ordtconnlem1  33958  lmdvg  33987  esumfsup  34104  reprsuc  34649  reprdifc  34661  bnj168  34763  bnj1185  34826  bnj1542  34890  bnj865  34956  bnj916  34966  bnj983  34984  bnj1176  35038  bnj1189  35042  bnj1296  35054  bnj1398  35067  bnj1450  35083  bnj1463  35088  nummin  35125  axregszf  35148  fineqvnttrclse  35165  onvf1odlem1  35168  loop1cycl  35202  cvmliftlem15  35363  cvmlift2lem12  35379  satfvsuclem2  35425  satfvsucsuc  35430  satfdm  35434  satf0  35437  dmopab3rexdif  35470  rexxfr3dALT  35704  dffr5  35819  dfon2lem9  35854  brbigcup  35961  elfuns  35978  brimage  35989  brimg  36000  dfrecs2  36015  imagesset  36018  brub  36019  brsegle  36173  sumeq2si  36267  prodeq2si  36269  cbvprodvw2  36312  filnetlem4  36446  bj-rexcom4bv  36947  bj-rexcom4b  36948  bj-elsngl  37033  bj-rest10  37153  bj-restreg  37164  bj-mpomptALT  37184  nlpineqsn  37473  fvineqsneq  37477  iundif1  37654  matunitlindflem1  37676  poimirlem1  37681  poimirlem30  37710  poimirlem32  37712  poimir  37713  ismblfin  37721  volsupnfl  37725  itg2addnclem3  37733  fdc  37805  isfldidl  38128  eldmqsres2  38346  n0elqs  38384  rnxrncnvepres  38467  rnxrnidres  38468  dfcoels  38552  br1cossinres  38569  br1cossinidres  38571  br1cossincnvepres  38572  br1cossxrnidres  38573  br1cossxrncnvepres  38574  br1cossxrncnvssrres  38620  eldmqs1cossres  38777  disjdmqscossss  38921  prtlem10  38984  prter2  39000  islshpat  39136  lshpsmreu  39228  2dim  39589  islpln5  39654  lplnexatN  39682  islvol5  39698  dalem18  39800  dalem20  39812  lhpexle2  40129  lhpexle3  40131  lhpex2leN  40132  4atex2  40196  4atex2-0bOLDN  40198  cdlemftr3  40684  cdlemg17pq  40791  cdlemg19  40803  cdlemg21  40805  cdlemg33d  40828  dva1dim  41104  dih1dimatlem  41448  dihglb2  41461  dvh2dim  41564  mapdrvallem2  41764  mapdpglem3  41794  hdmapglem7a  42046  hashnexinjle  42242  aks6d1c5  42252  supinf  42360  fimgmcyclem  42651  dffltz  42752  elrfirn  42812  isnacs2  42823  isnacs3  42827  sbc2rex  42904  4rexfrabdioph  42915  eldioph4b  42928  fphpd  42933  fiphp3d  42936  rencldnfilem  42937  rmxdioph  43133  expdiophlem1  43138  islnm2  43195  onmaxnelsup  43340  onsupnmax  43345  onsupuni  43346  onsupmaxb  43356  tfsconcatlem  43453  tfsconcatrn  43459  oadif1lem  43496  oadif1  43497  elimaint  43766  cnviun  43767  imaiun1  43768  coiun1  43769  elintima  43770  briunov2  43799  clsk3nimkb  44157  expandrexn  44408  prmunb2  44428  zfregs2VD  44957  n0abso  45093  sswfaxreg  45104  evth2f  45136  evthf  45148  ndisj2  45172  rexanuz2nf  45614  fnlimabslt  45801  climbddf  45809  limsupub  45826  limsuppnflem  45832  limsupubuz  45835  limsupre2lem  45846  limsupreuz  45859  limsupvaluz2  45860  cnrefiisplem  45951  cnrefiisp  45952  stoweidlem28  46150  fourierdlem63  46291  fourierdlem65  46293  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem100  46328  sge0pnfmpt  46567  ovn0  46688  smfaddlem1  46885  smflimlem4  46896  fsetsniunop  47173  2rexsb  47225  2rexrsb  47226  cbvrex2  47228  2reu8i  47237  clnbgrsym  47962  isubgr3stgrlem6  48095  copisnmnd  48293  pgrpgt2nabl  48490  islindeps  48578  lindslinindsimp1  48582  lindslinindsimp2  48588  islindeps2  48608  islininds2  48609  isldepslvec2  48610  ldepslinc  48634  sepnsepolem1  49046