Theorem rexbii 3108

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  r19.29imd  3126  r19.43  3129  3r19.43  3130  2rexbii  3137  rexnal2  3143  r19.42v  3193  r19.41vv  3231  3reeanv  3234  cbvrex2vw  3244  rexcom4a  3291  rexcom13  3294  rexrot4  3295  2ex2rexrot  3296  cbvrex2v  3355  rexcom4b  3484  ceqsrex2v  3617  clel5  3624  reu7  3694  2reu5a  3706  0el  4315  n0snor2el  4790  uni0b  4891  iuncom  4956  iuncom4  4957  iuniin  4961  dfiunv2  4990  iunab  5008  iunid  5017  iunsn  5022  iunn0  5023  iunin2  5027  iundif2  5030  iunun  5049  iunxiun  5053  iunpwss  5063  axrep6OLD  5236  inuni  5305  reusv2lem5  5358  iunopab  5528  dffr2  5606  dffr2ALT  5607  frc  5608  frminex  5624  dfepfr  5629  epfrc  5630  xpiundi  5716  xpiundir  5717  reliin  5788  iunxpf  5818  cnvuni  5860  dmiun  5887  dmopab2rex  5891  elres  6004  elidinxp  6030  dfima3  6049  dffr3  6085  rniun  6129  xpdifid  6150  dminxp  6162  imaco  6234  coiun  6240  imaindm  6282  dffr4  6303  frpomin2  6324  sucel  6418  isarep1  6606  rexrn  7064  ralrn  7065  elrnrexdmb  7067  fnasrn  7123  ralima  7217  reximaOLD  7219  ralimaOLD  7220  abrexco  7224  imaiun  7225  fliftcnv  7291  imaeqsexvOLD  7343  rexrnmpo  7532  imaeqexov  7630  iunpw  7750  abrexex2g  7941  el2xptp  8012  poxp2  8118  poxp3  8125  soseq  8134  frrlem9  8270  rdglem1  8381  tz7.49  8411  oarec  8526  omeu  8549  qsid  8758  eroveu  8789  ixp0  8909  fimax2g  9226  marypha2lem2  9379  dfsup2  9387  infcllem  9431  dfoi  9456  wemapsolem  9495  zfregcl  9539  zfregclOLD  9540  zfreg  9541  zfregfr  9556  oemapso  9634  brttrcl2  9666  ttrclresv  9669  zfregs2  9685  infenaleph  10044  isinfcard  10045  kmlem7  10110  kmlem13  10116  fin23lem26  10279  dffin1-5  10342  fin12  10367  numth  10426  ac6n  10439  zorn2lem7  10456  zorng  10458  brdom7disj  10485  brdom6disj  10486  uniwun  10695  axgroth5  10779  axgroth4  10787  grothprim  10789  npomex  10951  genpass  10964  elreal  11086  dfinfre  12170  infrenegsup  12172  uzwo  12909  ublbneg  12931  xrinfmss2  13311  4fvwrd4  13650  fsuppmapnn0fiubex  14002  fsuppmapnn0ub  14005  mptnn0fsuppr  14009  hashge2el2dif  14490  cshwsexa  14834  dfrtrclrec2  15068  rexanuz  15356  rexfiuz  15358  clim0  15516  cbvsum  15705  cbvsumv  15706  incexc2  15851  cbvprod  15926  cbvprodv  15927  prodeq1i  15929  fprodle  16009  iprodmul  16016  divalglem10  16419  divalgb  16421  ncoprmlnprm  16746  pythagtriplem2  16836  pythagtriplem19  16852  pythagtrip  16853  pceu  16865  prmreclem6  16940  4sqlem12  16975  cshwshashlem1  17114  cshwshash  17123  imasaddfnlem  17541  isdrs2  18321  chnfi  18649  smndex1mgm  18927  smndex1n0mnd  18932  pmtrprfvalrn  19511  pgpfac1lem5  20104  dvdsrval  20389  opprunit  20405  lsmspsn  21131  lsmelval2  21132  islpidl  21375  pzriprnglem3  21515  pzriprnglem10  21522  mat1dimelbas  22511  mat1dimbas  22512  mdetunilem8  22659  pmatcollpw2lem  22817  tgval2  22996  ntreq0  23117  isclo2  23128  neiptopnei  23172  ist0-3  23385  tgcmp  23441  cmpfi  23448  is1stc2  23482  unisngl  23567  xkobval  23626  txtube  23680  txcmplem1  23681  xkococnlem  23699  eltsms  24173  metrest  24564  iscau3  25320  bcth  25371  pmltpc  25492  itg2i1fseq  25797  itg2cn  25805  plyun0  26237  aaliou3lem9  26391  1cubr  26884  dchrvmasumlema  27541  selbergsb  27616  ostth  27680  noseponlem  27705  nosepon  27706  nolt02o  27736  noinfbnd1lem1  27764  noinfbnd1lem4  27767  cuteq1  27887  elold  27929  made0  27933  lrrecfr  28013  leadds1  28059  addsuniflem  28071  addsasslem1  28073  addsasslem2  28074  mulsrid  28183  mulsuniflem  28219  addsdilem1  28221  addsdilem2  28222  mulsasslem1  28233  mulsasslem2  28234  z12sge0  28553  elreno2  28565  renegscl  28568  istrkg2ld  28606  tglowdim1i  28647  legtrid  28737  midex  28883  ishpg  28905  brbtwn2  29052  colinearalg  29057  ax5seg  29085  axpasch  29088  axlowdimlem6  29094  axeuclidlem  29109  axeuclid  29110  elntg2  29132  umgr2edg1  29358  umgr2edgneu  29361  nbgrsym  29510  isuvtx  29542  usgr2pth0  29911  wlkiswwlksupgr2  30023  clwwlknun  30260  4cycl2vnunb  30438  fusgreg2wsp  30484  lpni  30629  nmobndseqi  30928  hhcmpl  31349  shne0i  31597  nmcopexi  32176  nmcfnexi  32200  cdj3lem3b  32589  rexcom4f  32615  reuxfrdf  32638  iunin1f  32706  ofpreima  32817  intimafv  32863  fpwrelmapffslem  32884  tosglblem  33113  xrnarchi  33325  isunit2  33381  isdrng4  33443  dvdsrspss  33534  lsmsnorb  33538  lsmsnorb2  33539  1arithufdlem4  33704  constrconj  34003  ordtconnlem1  34182  lmdvg  34211  esumfsup  34328  reprsuc  34873  reprdifc  34885  bnj168  34990  bnj1185  35052  bnj1542  35116  bnj865  35182  bnj916  35192  bnj983  35210  bnj1176  35264  bnj1189  35268  bnj1296  35280  bnj1398  35293  bnj1450  35309  bnj1463  35314  nummin  35353  fineqvnttrclse  35384  axregszf  35389  onvf1odlem1  35410  loop1cycl  35451  cvmliftlem15  35612  cvmlift2lem12  35628  satfvsuclem2  35674  satfvsucsuc  35679  satfdm  35683  satf0  35686  dmopab3rexdif  35719  rexxfr3dALT  35953  dffr5  36068  dfon2lem9  36103  brbigcup  36210  elfuns  36227  brimage  36238  brimg  36249  dfrecs2  36264  imagesset  36267  brub  36268  brsegle  36422  sumeq2si  36526  prodeq2si  36528  cbvprodvw2  36571  filnetlem4  36705  bj-rexcom4bv  37331  bj-rexcom4b  37332  bj-elsngl  37417  bj-axseprep  37523  bj-rest10  37542  bj-restreg  37553  bj-mpomptALT  37573  nlpineqsn  37866  fvineqsneq  37870  iundif1  38057  matunitlindflem1  38079  poimirlem1  38084  poimirlem30  38113  poimirlem32  38115  poimir  38116  ismblfin  38124  volsupnfl  38128  itg2addnclem3  38136  fdc  38208  isfldidl  38531  eldmqsres2  38757  n0elqs  38795  rnxrncnvepres  38886  rnxrnidres  38887  dfcoels  38983  br1cossinres  39000  br1cossinidres  39002  br1cossincnvepres  39003  br1cossxrnidres  39004  br1cossxrncnvepres  39005  br1cossxrncnvssrres  39051  eldmqs1cossres  39207  disjdmqscossss  39369  prtlem10  39453  prter2  39469  islshpat  39605  lshpsmreu  39697  2dim  40058  islpln5  40123  lplnexatN  40151  islvol5  40167  dalem18  40269  dalem20  40281  lhpexle2  40598  lhpexle3  40600  lhpex2leN  40601  4atex2  40665  4atex2-0bOLDN  40667  cdlemftr3  41153  cdlemg17pq  41260  cdlemg19  41272  cdlemg21  41274  cdlemg33d  41297  dva1dim  41573  dih1dimatlem  41917  dihglb2  41930  dvh2dim  42033  mapdrvallem2  42233  mapdpglem3  42263  hdmapglem7a  42515  hashnexinjle  42710  aks6d1c5  42720  supinf  42822  fimgmcyclem  43115  dffltz  43180  elrfirn  43240  isnacs2  43251  isnacs3  43255  sbc2rex  43330  4rexfrabdioph  43339  eldioph4b  43352  fphpd  43357  fiphp3d  43360  rencldnfilem  43361  rmxdioph  43557  expdiophlem1  43562  islnm2  43619  onmaxnelsup  43764  onsupnmax  43769  onsupuni  43770  onsupmaxb  43780  tfsconcatlem  43877  tfsconcatrn  43883  oadif1lem  43920  oadif1  43921  elimaint  44189  cnviun  44190  imaiun1  44191  coiun1  44192  elintima  44193  briunov2  44222  clsk3nimkb  44580  expandrexn  44831  prmunb2  44851  zfregs2VD  45380  n0abso  45516  sswfaxreg  45527  evth2f  45559  evthf  45571  ndisj2  45595  rexanuz2nf  46030  fnlimabslt  46217  climbddf  46225  limsupub  46242  limsuppnflem  46248  limsupubuz  46251  limsupre2lem  46262  limsupreuz  46275  limsupvaluz2  46276  cnrefiisplem  46367  cnrefiisp  46368  stoweidlem28  46566  fourierdlem63  46707  fourierdlem65  46709  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem100  46744  sge0pnfmpt  46983  ovn0  47104  smfaddlem1  47301  smflimlem4  47312  fsetsniunop  47607  2rexsb  47659  2rexrsb  47660  cbvrex2  47662  2reu8i  47671  clnbgrsym  48424  isubgr3stgrlem6  48557  copisnmnd  48755  pgrpgt2nabl  48952  islindeps  49039  lindslinindsimp1  49043  lindslinindsimp2  49049  islindeps2  49069  islininds2  49070  isldepslvec2  49071  ldepslinc  49095  sepnsepolem1  49507