Theorem rexbii 3100

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.29imd  3124  r19.43  3128  2rexbii  3135  rexnal2  3141  r19.42v  3197  r19.41vv  3233  3reeanv  3236  2ralorOLD  3238  cbvrex2vw  3248  rexcomOLD  3297  rexcom4a  3298  rexcom13  3302  rexrot4  3303  2ex2rexrot  3304  cbvrex2v  3377  rexcom4b  3521  ceqsrex2v  3671  clel5  3678  reu7  3754  2reu5a  3766  0el  4386  n0snor2el  4858  uni0b  4957  iuncom  5022  iuncom4  5023  iuniin  5027  dfiunv2  5058  iunab  5074  iunid  5083  iunsn  5089  iunn0  5090  iunin2  5094  iundif2  5097  iunun  5116  iunxiun  5120  iunpwss  5130  axrep6  5310  inuni  5368  reusv2lem5  5420  iunopab  5578  iunopabOLD  5579  dffr2  5661  dffr2ALT  5662  frc  5663  frminex  5679  dfepfr  5684  epfrc  5685  xpiundi  5770  xpiundir  5771  reliin  5841  iunxpf  5873  cnvuni  5911  dmiun  5938  dmopab2rex  5942  elres  6049  elidinxp  6073  dfima3  6092  dffr3  6129  rniun  6179  xpdifid  6199  dminxp  6211  imaco  6282  coiun  6287  imaindm  6330  dffr4  6352  frpomin2  6373  tz6.26OLD  6380  sucel  6469  isarep1  6667  isarep1OLD  6668  rexrn  7121  ralrn  7122  elrnrexdmb  7124  fnasrn  7179  ralima  7274  reximaOLD  7276  ralimaOLD  7277  abrexco  7281  imaiun  7282  fliftcnv  7347  imaeqsexvOLD  7399  rexrnmpo  7590  imaeqexov  7688  iunpw  7806  abrexex2g  8005  el2xptp  8076  poxp2  8184  poxp3  8191  soseq  8200  frrlem9  8335  rdglem1  8471  tz7.49  8501  oarec  8618  omeu  8641  qsid  8841  eroveu  8870  ixp0  8989  fimax2g  9350  marypha2lem2  9505  dfsup2  9513  infcllem  9556  dfoi  9580  wemapsolem  9619  zfregcl  9663  zfreg  9664  zfregfr  9674  oemapso  9751  brttrcl2  9783  ttrclresv  9786  zfregs2  9802  infenaleph  10160  isinfcard  10161  kmlem7  10226  kmlem13  10232  fin23lem26  10394  dffin1-5  10457  fin12  10482  numth  10541  ac6n  10554  zorn2lem7  10571  zorng  10573  brdom7disj  10600  brdom6disj  10601  uniwun  10809  axgroth5  10893  axgroth4  10901  grothprim  10903  npomex  11065  genpass  11078  elreal  11200  dfinfre  12276  infrenegsup  12278  uzwo  12976  ublbneg  12998  xrinfmss2  13373  4fvwrd4  13705  fsuppmapnn0fiubex  14043  fsuppmapnn0ub  14046  mptnn0fsuppr  14050  hashge2el2dif  14529  cshwsexa  14872  dfrtrclrec2  15107  rexanuz  15394  rexfiuz  15396  clim0  15552  cbvsum  15743  cbvsumv  15744  incexc2  15886  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  fprodle  16044  iprodmul  16051  divalglem10  16450  divalgb  16452  ncoprmlnprm  16775  pythagtriplem2  16864  pythagtriplem19  16880  pythagtrip  16881  pceu  16893  prmreclem6  16968  4sqlem12  17003  cshwshashlem1  17143  cshwshash  17152  imasaddfnlem  17588  isdrs2  18376  smndex1mgm  18942  smndex1n0mnd  18947  pmtrprfvalrn  19530  pgpfac1lem5  20123  dvdsrval  20387  opprunit  20403  lsmspsn  21106  lsmelval2  21107  islpidl  21358  pzriprnglem3  21517  pzriprnglem10  21524  mat1dimelbas  22498  mat1dimbas  22499  mdetunilem8  22646  pmatcollpw2lem  22804  tgval2  22984  ntreq0  23106  isclo2  23117  neiptopnei  23161  ist0-3  23374  tgcmp  23430  cmpfi  23437  is1stc2  23471  unisngl  23556  xkobval  23615  txtube  23669  txcmplem1  23670  xkococnlem  23688  eltsms  24162  metrest  24558  iscau3  25331  bcth  25382  pmltpc  25504  itg2i1fseq  25810  itg2cn  25818  plyun0  26256  aaliou3lem9  26410  1cubr  26903  dchrvmasumlema  27562  selbergsb  27637  ostth  27701  noseponlem  27727  nosepon  27728  nolt02o  27758  noinfbnd1lem1  27786  noinfbnd1lem4  27789  cuteq1  27896  elold  27926  made0  27930  lrrecfr  27994  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  mulsrid  28157  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  istrkg2ld  28486  tglowdim1i  28527  legtrid  28617  midex  28763  ishpg  28785  brbtwn2  28938  colinearalg  28943  ax5seg  28971  axpasch  28974  axlowdimlem6  28980  axeuclidlem  28995  axeuclid  28996  elntg2  29018  umgr2edg1  29246  umgr2edgneu  29249  nbgrsym  29398  isuvtx  29430  usgr2pth0  29801  wlkiswwlksupgr2  29910  clwwlknun  30144  4cycl2vnunb  30322  fusgreg2wsp  30368  lpni  30512  nmobndseqi  30811  hhcmpl  31232  shne0i  31480  nmcopexi  32059  nmcfnexi  32083  cdj3lem3b  32472  rexcom4f  32497  reuxfrdf  32519  iunin1f  32580  ofpreima  32683  intimafv  32722  fpwrelmapffslem  32746  tosglblem  32947  xrnarchi  33164  isunit2  33220  isdrng4  33264  dvdsrspss  33380  lsmsnorb  33384  lsmsnorb2  33385  1arithufdlem4  33540  constrconj  33735  ordtconnlem1  33870  lmdvg  33899  esumfsup  34034  reprsuc  34592  reprdifc  34604  bnj168  34706  bnj1185  34769  bnj1542  34833  bnj865  34899  bnj916  34909  bnj983  34927  bnj1176  34981  bnj1189  34985  bnj1296  34997  bnj1398  35010  bnj1450  35026  bnj1463  35031  nummin  35067  loop1cycl  35105  cvmliftlem15  35266  cvmlift2lem12  35282  satfvsuclem2  35328  satfvsucsuc  35333  satfdm  35337  satf0  35340  dmopab3rexdif  35373  rexxfr3dALT  35607  dffr5  35716  dfon2lem9  35755  brbigcup  35862  elfuns  35879  brimage  35890  brimg  35901  dfrecs2  35914  imagesset  35917  brub  35918  brsegle  36072  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36213  filnetlem4  36347  bj-rexcom4bv  36848  bj-rexcom4b  36849  bj-elsngl  36934  bj-rest10  37054  bj-restreg  37065  bj-mpomptALT  37085  nlpineqsn  37374  fvineqsneq  37378  iundif1  37554  matunitlindflem1  37576  poimirlem1  37581  poimirlem30  37610  poimirlem32  37612  poimir  37613  ismblfin  37621  volsupnfl  37625  itg2addnclem3  37633  fdc  37705  isfldidl  38028  eldmqsres2  38244  n0elqs  38282  rnxrncnvepres  38356  rnxrnidres  38357  dfcoels  38386  br1cossinres  38403  br1cossinidres  38405  br1cossincnvepres  38406  br1cossxrnidres  38407  br1cossxrncnvepres  38408  br1cossxrncnvssrres  38464  eldmqs1cossres  38615  disjdmqscossss  38759  prtlem10  38821  prter2  38837  islshpat  38973  lshpsmreu  39065  2dim  39427  islpln5  39492  lplnexatN  39520  islvol5  39536  dalem18  39638  dalem20  39650  lhpexle2  39967  lhpexle3  39969  lhpex2leN  39970  4atex2  40034  4atex2-0bOLDN  40036  cdlemftr3  40522  cdlemg17pq  40629  cdlemg19  40641  cdlemg21  40643  cdlemg33d  40666  dva1dim  40942  dih1dimatlem  41286  dihglb2  41299  dvh2dim  41402  mapdrvallem2  41602  mapdpglem3  41632  hdmapglem7a  41884  hashnexinjle  42086  aks6d1c5  42096  supinf  42237  fimgmcyclem  42488  dffltz  42589  elrfirn  42651  isnacs2  42662  isnacs3  42666  sbc2rex  42743  4rexfrabdioph  42754  eldioph4b  42767  fphpd  42772  fiphp3d  42775  rencldnfilem  42776  rmxdioph  42973  expdiophlem1  42978  islnm2  43035  onmaxnelsup  43184  onsupnmax  43189  onsupuni  43190  onsupmaxb  43200  tfsconcatlem  43298  tfsconcatrn  43304  oadif1lem  43341  oadif1  43342  elimaint  43611  cnviun  43612  imaiun1  43613  coiun1  43614  elintima  43615  briunov2  43644  clsk3nimkb  44002  expandrexn  44260  prmunb2  44280  zfregs2VD  44812  evth2f  44915  evthf  44927  ndisj2  44953  rexanuz2nf  45408  fnlimabslt  45600  climbddf  45608  limsupub  45625  limsuppnflem  45631  limsupubuz  45634  limsupre2lem  45645  limsupreuz  45658  limsupvaluz2  45659  cnrefiisplem  45750  cnrefiisp  45751  stoweidlem28  45949  fourierdlem63  46090  fourierdlem65  46092  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem100  46127  sge0pnfmpt  46366  ovn0  46487  smfaddlem1  46684  smflimlem4  46695  fsetsniunop  46964  2rexsb  47016  2rexrsb  47017  cbvrex2  47019  2reu8i  47028  clnbgrsym  47710  copisnmnd  47892  pgrpgt2nabl  48091  islindeps  48182  lindslinindsimp1  48186  lindslinindsimp2  48192  islindeps2  48212  islininds2  48213  isldepslvec2  48214  ldepslinc  48238  sepnsepolem1  48601