Theorem rexbii 3083

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

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

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 3061

This theorem is referenced by:  r19.29imd  3101  r19.43  3104  3r19.43  3105  2rexbii  3112  rexnal2  3118  r19.42v  3168  r19.41vv  3206  3reeanv  3209  cbvrex2vw  3219  rexcom4a  3266  rexcom13  3269  rexrot4  3270  2ex2rexrot  3271  cbvrex2v  3339  rexcom4b  3472  ceqsrex2v  3612  clel5  3619  reu7  3690  2reu5a  3702  0el  4315  n0snor2el  4789  uni0b  4889  iuncom  4954  iuncom4  4955  iuniin  4959  dfiunv2  4989  iunab  5007  iunid  5016  iunsn  5021  iunn0  5022  iunin2  5026  iundif2  5029  iunun  5048  iunxiun  5052  iunpwss  5062  axrep6OLD  5234  inuni  5295  reusv2lem5  5347  iunopab  5507  dffr2  5585  dffr2ALT  5586  frc  5587  frminex  5603  dfepfr  5608  epfrc  5609  xpiundi  5695  xpiundir  5696  reliin  5766  iunxpf  5797  cnvuni  5835  dmiun  5862  dmopab2rex  5866  elres  5979  elidinxp  6003  dfima3  6022  dffr3  6058  rniun  6105  xpdifid  6126  dminxp  6138  imaco  6209  coiun  6215  imaindm  6257  dffr4  6278  frpomin2  6299  sucel  6393  isarep1  6581  rexrn  7032  ralrn  7033  elrnrexdmb  7035  fnasrn  7090  ralima  7183  reximaOLD  7185  ralimaOLD  7186  abrexco  7190  imaiun  7191  fliftcnv  7257  imaeqsexvOLD  7309  rexrnmpo  7498  imaeqexov  7596  iunpw  7716  abrexex2g  7908  el2xptp  7979  poxp2  8085  poxp3  8092  soseq  8101  frrlem9  8236  rdglem1  8346  tz7.49  8376  oarec  8489  omeu  8512  qsid  8718  eroveu  8749  ixp0  8869  fimax2g  9186  marypha2lem2  9339  dfsup2  9347  infcllem  9391  dfoi  9416  wemapsolem  9455  zfregcl  9499  zfregclOLD  9500  zfreg  9501  zfregfr  9513  oemapso  9591  brttrcl2  9623  ttrclresv  9626  zfregs2  9642  infenaleph  10001  isinfcard  10002  kmlem7  10067  kmlem13  10073  fin23lem26  10235  dffin1-5  10298  fin12  10323  numth  10382  ac6n  10395  zorn2lem7  10412  zorng  10414  brdom7disj  10441  brdom6disj  10442  uniwun  10651  axgroth5  10735  axgroth4  10743  grothprim  10745  npomex  10907  genpass  10920  elreal  11042  dfinfre  12123  infrenegsup  12125  uzwo  12824  ublbneg  12846  xrinfmss2  13226  4fvwrd4  13564  fsuppmapnn0fiubex  13915  fsuppmapnn0ub  13918  mptnn0fsuppr  13922  hashge2el2dif  14403  cshwsexa  14747  dfrtrclrec2  14981  rexanuz  15269  rexfiuz  15271  clim0  15429  cbvsum  15618  cbvsumv  15619  incexc2  15761  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  fprodle  15919  iprodmul  15926  divalglem10  16329  divalgb  16331  ncoprmlnprm  16655  pythagtriplem2  16745  pythagtriplem19  16761  pythagtrip  16762  pceu  16774  prmreclem6  16849  4sqlem12  16884  cshwshashlem1  17023  cshwshash  17032  imasaddfnlem  17449  isdrs2  18229  chnfi  18557  smndex1mgm  18832  smndex1n0mnd  18837  pmtrprfvalrn  19417  pgpfac1lem5  20010  dvdsrval  20297  opprunit  20313  lsmspsn  21036  lsmelval2  21037  islpidl  21280  pzriprnglem3  21438  pzriprnglem10  21445  mat1dimelbas  22415  mat1dimbas  22416  mdetunilem8  22563  pmatcollpw2lem  22721  tgval2  22900  ntreq0  23021  isclo2  23032  neiptopnei  23076  ist0-3  23289  tgcmp  23345  cmpfi  23352  is1stc2  23386  unisngl  23471  xkobval  23530  txtube  23584  txcmplem1  23585  xkococnlem  23603  eltsms  24077  metrest  24468  iscau3  25234  bcth  25285  pmltpc  25407  itg2i1fseq  25712  itg2cn  25720  plyun0  26158  aaliou3lem9  26314  1cubr  26808  dchrvmasumlema  27467  selbergsb  27542  ostth  27606  noseponlem  27632  nosepon  27633  nolt02o  27663  noinfbnd1lem1  27691  noinfbnd1lem4  27694  cuteq1  27813  elold  27855  made0  27859  lrrecfr  27939  leadds1  27985  addsuniflem  27997  addsasslem1  27999  addsasslem2  28000  mulsrid  28109  mulsuniflem  28145  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  z12sge0  28479  elreno2  28491  renegscl  28494  istrkg2ld  28532  tglowdim1i  28573  legtrid  28663  midex  28809  ishpg  28831  brbtwn2  28978  colinearalg  28983  ax5seg  29011  axpasch  29014  axlowdimlem6  29020  axeuclidlem  29035  axeuclid  29036  elntg2  29058  umgr2edg1  29284  umgr2edgneu  29287  nbgrsym  29436  isuvtx  29468  usgr2pth0  29838  wlkiswwlksupgr2  29950  clwwlknun  30187  4cycl2vnunb  30365  fusgreg2wsp  30411  lpni  30555  nmobndseqi  30854  hhcmpl  31275  shne0i  31523  nmcopexi  32102  nmcfnexi  32126  cdj3lem3b  32515  rexcom4f  32542  reuxfrdf  32565  iunin1f  32632  ofpreima  32743  intimafv  32790  fpwrelmapffslem  32811  tosglblem  33056  xrnarchi  33266  isunit2  33322  isdrng4  33377  dvdsrspss  33468  lsmsnorb  33472  lsmsnorb2  33473  1arithufdlem4  33628  constrconj  33902  ordtconnlem1  34081  lmdvg  34110  esumfsup  34227  reprsuc  34772  reprdifc  34784  bnj168  34886  bnj1185  34949  bnj1542  35013  bnj865  35079  bnj916  35089  bnj983  35107  bnj1176  35161  bnj1189  35165  bnj1296  35177  bnj1398  35190  bnj1450  35206  bnj1463  35211  nummin  35249  fineqvnttrclse  35280  axregszf  35285  onvf1odlem1  35297  loop1cycl  35331  cvmliftlem15  35492  cvmlift2lem12  35508  satfvsuclem2  35554  satfvsucsuc  35559  satfdm  35563  satf0  35566  dmopab3rexdif  35599  rexxfr3dALT  35833  dffr5  35948  dfon2lem9  35983  brbigcup  36090  elfuns  36107  brimage  36118  brimg  36129  dfrecs2  36144  imagesset  36147  brub  36148  brsegle  36302  sumeq2si  36396  prodeq2si  36398  cbvprodvw2  36441  filnetlem4  36575  bj-rexcom4bv  37083  bj-rexcom4b  37084  bj-elsngl  37169  bj-rest10  37289  bj-restreg  37300  bj-mpomptALT  37320  nlpineqsn  37609  fvineqsneq  37613  iundif1  37791  matunitlindflem1  37813  poimirlem1  37818  poimirlem30  37847  poimirlem32  37849  poimir  37850  ismblfin  37858  volsupnfl  37862  itg2addnclem3  37870  fdc  37942  isfldidl  38265  eldmqsres2  38483  n0elqs  38521  rnxrncnvepres  38604  rnxrnidres  38605  dfcoels  38689  br1cossinres  38706  br1cossinidres  38708  br1cossincnvepres  38709  br1cossxrnidres  38710  br1cossxrncnvepres  38711  br1cossxrncnvssrres  38757  eldmqs1cossres  38914  disjdmqscossss  39058  prtlem10  39121  prter2  39137  islshpat  39273  lshpsmreu  39365  2dim  39726  islpln5  39791  lplnexatN  39819  islvol5  39835  dalem18  39937  dalem20  39949  lhpexle2  40266  lhpexle3  40268  lhpex2leN  40269  4atex2  40333  4atex2-0bOLDN  40335  cdlemftr3  40821  cdlemg17pq  40928  cdlemg19  40940  cdlemg21  40942  cdlemg33d  40965  dva1dim  41241  dih1dimatlem  41585  dihglb2  41598  dvh2dim  41701  mapdrvallem2  41901  mapdpglem3  41931  hdmapglem7a  42183  hashnexinjle  42379  aks6d1c5  42389  supinf  42493  fimgmcyclem  42784  dffltz  42873  elrfirn  42933  isnacs2  42944  isnacs3  42948  sbc2rex  43025  4rexfrabdioph  43036  eldioph4b  43049  fphpd  43054  fiphp3d  43057  rencldnfilem  43058  rmxdioph  43254  expdiophlem1  43259  islnm2  43316  onmaxnelsup  43461  onsupnmax  43466  onsupuni  43467  onsupmaxb  43477  tfsconcatlem  43574  tfsconcatrn  43580  oadif1lem  43617  oadif1  43618  elimaint  43886  cnviun  43887  imaiun1  43888  coiun1  43889  elintima  43890  briunov2  43919  clsk3nimkb  44277  expandrexn  44528  prmunb2  44548  zfregs2VD  45077  n0abso  45213  sswfaxreg  45224  evth2f  45256  evthf  45268  ndisj2  45292  rexanuz2nf  45732  fnlimabslt  45919  climbddf  45927  limsupub  45944  limsuppnflem  45950  limsupubuz  45953  limsupre2lem  45964  limsupreuz  45977  limsupvaluz2  45978  cnrefiisplem  46069  cnrefiisp  46070  stoweidlem28  46268  fourierdlem63  46409  fourierdlem65  46411  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem100  46446  sge0pnfmpt  46685  ovn0  46806  smfaddlem1  47003  smflimlem4  47014  fsetsniunop  47291  2rexsb  47343  2rexrsb  47344  cbvrex2  47346  2reu8i  47355  clnbgrsym  48080  isubgr3stgrlem6  48213  copisnmnd  48411  pgrpgt2nabl  48608  islindeps  48695  lindslinindsimp1  48699  lindslinindsimp2  48705  islindeps2  48725  islininds2  48726  isldepslvec2  48727  ldepslinc  48751  sepnsepolem1  49163