Theorem rexbii 3078

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∃wrex 3055

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3056

This theorem is referenced by:  r19.29imd  3100  r19.43  3103  3r19.43  3104  2rexbii  3111  rexnal2  3117  r19.42v  3171  r19.41vv  3209  3reeanv  3212  cbvrex2vw  3222  rexcomOLD  3269  rexcom4a  3270  rexcom13  3274  rexrot4  3275  2ex2rexrot  3276  cbvrex2v  3346  rexcom4b  3488  ceqsrex2v  3633  clel5  3640  reu7  3711  2reu5a  3723  0el  4334  n0snor2el  4805  uni0b  4905  iuncom  4971  iuncom4  4972  iuniin  4976  dfiunv2  5007  iunab  5023  iunid  5032  iunsn  5038  iunn0  5039  iunin2  5043  iundif2  5046  iunun  5065  iunxiun  5069  iunpwss  5079  axrep6OLD  5252  inuni  5313  reusv2lem5  5365  iunopab  5527  iunopabOLD  5528  dffr2  5607  dffr2ALT  5608  frc  5609  frminex  5625  dfepfr  5630  epfrc  5631  xpiundi  5717  xpiundir  5718  reliin  5788  iunxpf  5820  cnvuni  5858  dmiun  5885  dmopab2rex  5889  elres  5999  elidinxp  6023  dfima3  6042  dffr3  6078  rniun  6128  xpdifid  6149  dminxp  6161  imaco  6232  coiun  6237  imaindm  6280  dffr4  6301  frpomin2  6322  sucel  6416  isarep1  6614  isarep1OLD  6615  rexrn  7066  ralrn  7067  elrnrexdmb  7069  fnasrn  7124  ralima  7218  reximaOLD  7220  ralimaOLD  7221  abrexco  7225  imaiun  7226  fliftcnv  7293  imaeqsexvOLD  7345  rexrnmpo  7536  imaeqexov  7634  iunpw  7754  abrexex2g  7952  el2xptp  8023  poxp2  8131  poxp3  8138  soseq  8147  frrlem9  8282  rdglem1  8392  tz7.49  8422  oarec  8537  omeu  8560  qsid  8760  eroveu  8789  ixp0  8908  fimax2g  9251  marypha2lem2  9405  dfsup2  9413  infcllem  9457  dfoi  9482  wemapsolem  9521  zfregcl  9565  zfreg  9566  zfregfr  9576  oemapso  9653  brttrcl2  9685  ttrclresv  9688  zfregs2  9704  infenaleph  10062  isinfcard  10063  kmlem7  10128  kmlem13  10134  fin23lem26  10296  dffin1-5  10359  fin12  10384  numth  10443  ac6n  10456  zorn2lem7  10473  zorng  10475  brdom7disj  10502  brdom6disj  10503  uniwun  10711  axgroth5  10795  axgroth4  10803  grothprim  10805  npomex  10967  genpass  10980  elreal  11102  dfinfre  12180  infrenegsup  12182  uzwo  12884  ublbneg  12906  xrinfmss2  13284  4fvwrd4  13622  fsuppmapnn0fiubex  13967  fsuppmapnn0ub  13970  mptnn0fsuppr  13974  hashge2el2dif  14455  cshwsexa  14799  dfrtrclrec2  15034  rexanuz  15321  rexfiuz  15323  clim0  15479  cbvsum  15668  cbvsumv  15669  incexc2  15811  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  fprodle  15969  iprodmul  15976  divalglem10  16378  divalgb  16380  ncoprmlnprm  16704  pythagtriplem2  16794  pythagtriplem19  16810  pythagtrip  16811  pceu  16823  prmreclem6  16898  4sqlem12  16933  cshwshashlem1  17072  cshwshash  17081  imasaddfnlem  17497  isdrs2  18273  smndex1mgm  18840  smndex1n0mnd  18845  pmtrprfvalrn  19424  pgpfac1lem5  20017  dvdsrval  20276  opprunit  20292  lsmspsn  20997  lsmelval2  20998  islpidl  21241  pzriprnglem3  21399  pzriprnglem10  21406  mat1dimelbas  22364  mat1dimbas  22365  mdetunilem8  22512  pmatcollpw2lem  22670  tgval2  22849  ntreq0  22970  isclo2  22981  neiptopnei  23025  ist0-3  23238  tgcmp  23294  cmpfi  23301  is1stc2  23335  unisngl  23420  xkobval  23479  txtube  23533  txcmplem1  23534  xkococnlem  23552  eltsms  24026  metrest  24418  iscau3  25185  bcth  25236  pmltpc  25358  itg2i1fseq  25663  itg2cn  25671  plyun0  26109  aaliou3lem9  26265  1cubr  26759  dchrvmasumlema  27418  selbergsb  27493  ostth  27557  noseponlem  27583  nosepon  27584  nolt02o  27614  noinfbnd1lem1  27642  noinfbnd1lem4  27645  cuteq1  27753  elold  27788  made0  27792  lrrecfr  27857  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  mulsrid  28023  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  zs12ge0  28349  renegscl  28356  istrkg2ld  28394  tglowdim1i  28435  legtrid  28525  midex  28671  ishpg  28693  brbtwn2  28839  colinearalg  28844  ax5seg  28872  axpasch  28875  axlowdimlem6  28881  axeuclidlem  28896  axeuclid  28897  elntg2  28919  umgr2edg1  29145  umgr2edgneu  29148  nbgrsym  29297  isuvtx  29329  usgr2pth0  29702  wlkiswwlksupgr2  29814  clwwlknun  30048  4cycl2vnunb  30226  fusgreg2wsp  30272  lpni  30416  nmobndseqi  30715  hhcmpl  31136  shne0i  31384  nmcopexi  31963  nmcfnexi  31987  cdj3lem3b  32376  rexcom4f  32404  reuxfrdf  32427  iunin1f  32493  ofpreima  32597  intimafv  32642  fpwrelmapffslem  32663  tosglblem  32908  xrnarchi  33146  isunit2  33199  isdrng4  33253  dvdsrspss  33366  lsmsnorb  33370  lsmsnorb2  33371  1arithufdlem4  33526  constrconj  33743  ordtconnlem1  33922  lmdvg  33951  esumfsup  34068  reprsuc  34614  reprdifc  34626  bnj168  34728  bnj1185  34791  bnj1542  34855  bnj865  34921  bnj916  34931  bnj983  34949  bnj1176  35003  bnj1189  35007  bnj1296  35019  bnj1398  35032  bnj1450  35048  bnj1463  35053  nummin  35089  loop1cycl  35126  cvmliftlem15  35287  cvmlift2lem12  35303  satfvsuclem2  35349  satfvsucsuc  35354  satfdm  35358  satf0  35361  dmopab3rexdif  35394  rexxfr3dALT  35628  dffr5  35738  dfon2lem9  35776  brbigcup  35883  elfuns  35900  brimage  35911  brimg  35922  dfrecs2  35935  imagesset  35938  brub  35939  brsegle  36093  sumeq2si  36187  prodeq2si  36189  cbvprodvw2  36232  filnetlem4  36366  bj-rexcom4bv  36867  bj-rexcom4b  36868  bj-elsngl  36953  bj-rest10  37073  bj-restreg  37084  bj-mpomptALT  37104  nlpineqsn  37393  fvineqsneq  37397  iundif1  37585  matunitlindflem1  37607  poimirlem1  37612  poimirlem30  37641  poimirlem32  37643  poimir  37644  ismblfin  37652  volsupnfl  37656  itg2addnclem3  37664  fdc  37736  isfldidl  38059  eldmqsres2  38273  n0elqs  38311  rnxrncnvepres  38385  rnxrnidres  38386  dfcoels  38415  br1cossinres  38432  br1cossinidres  38434  br1cossincnvepres  38435  br1cossxrnidres  38436  br1cossxrncnvepres  38437  br1cossxrncnvssrres  38493  eldmqs1cossres  38644  disjdmqscossss  38788  prtlem10  38850  prter2  38866  islshpat  39002  lshpsmreu  39094  2dim  39456  islpln5  39521  lplnexatN  39549  islvol5  39565  dalem18  39667  dalem20  39679  lhpexle2  39996  lhpexle3  39998  lhpex2leN  39999  4atex2  40063  4atex2-0bOLDN  40065  cdlemftr3  40551  cdlemg17pq  40658  cdlemg19  40670  cdlemg21  40672  cdlemg33d  40695  dva1dim  40971  dih1dimatlem  41315  dihglb2  41328  dvh2dim  41431  mapdrvallem2  41631  mapdpglem3  41661  hdmapglem7a  41913  hashnexinjle  42109  aks6d1c5  42119  supinf  42222  fimgmcyclem  42493  dffltz  42594  elrfirn  42655  isnacs2  42666  isnacs3  42670  sbc2rex  42747  4rexfrabdioph  42758  eldioph4b  42771  fphpd  42776  fiphp3d  42779  rencldnfilem  42780  rmxdioph  42977  expdiophlem1  42982  islnm2  43039  onmaxnelsup  43184  onsupnmax  43189  onsupuni  43190  onsupmaxb  43200  tfsconcatlem  43297  tfsconcatrn  43303  oadif1lem  43340  oadif1  43341  elimaint  43610  cnviun  43611  imaiun1  43612  coiun1  43613  elintima  43614  briunov2  43643  clsk3nimkb  44001  expandrexn  44252  prmunb2  44272  zfregs2VD  44802  n0abso  44938  sswfaxreg  44949  evth2f  44981  evthf  44993  ndisj2  45017  rexanuz2nf  45461  fnlimabslt  45650  climbddf  45658  limsupub  45675  limsuppnflem  45681  limsupubuz  45684  limsupre2lem  45695  limsupreuz  45708  limsupvaluz2  45709  cnrefiisplem  45800  cnrefiisp  45801  stoweidlem28  45999  fourierdlem63  46140  fourierdlem65  46142  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem100  46177  sge0pnfmpt  46416  ovn0  46537  smfaddlem1  46734  smflimlem4  46745  fsetsniunop  47020  2rexsb  47072  2rexrsb  47073  cbvrex2  47075  2reu8i  47084  clnbgrsym  47793  isubgr3stgrlem6  47925  copisnmnd  48086  pgrpgt2nabl  48283  islindeps  48371  lindslinindsimp1  48375  lindslinindsimp2  48381  islindeps2  48401  islininds2  48402  isldepslvec2  48403  ldepslinc  48427  sepnsepolem1  48838