Theorem rexbii 3085

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.29imd  3103  r19.43  3106  3r19.43  3107  2rexbii  3114  rexnal2  3120  r19.42v  3170  r19.41vv  3208  3reeanv  3211  cbvrex2vw  3221  rexcom4a  3268  rexcom13  3271  rexrot4  3272  2ex2rexrot  3273  cbvrex2v  3332  rexcom4b  3462  ceqsrex2v  3601  clel5  3608  reu7  3679  2reu5a  3691  0el  4304  n0snor2el  4777  uni0b  4877  iuncom  4942  iuncom4  4943  iuniin  4947  dfiunv2  4977  iunab  4995  iunid  5004  iunsn  5009  iunn0  5010  iunin2  5014  iundif2  5017  iunun  5036  iunxiun  5040  iunpwss  5050  axrep6OLD  5222  inuni  5287  reusv2lem5  5339  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  7033  ralrn  7034  elrnrexdmb  7036  fnasrn  7092  ralima  7185  reximaOLD  7187  ralimaOLD  7188  abrexco  7192  imaiun  7193  fliftcnv  7259  imaeqsexvOLD  7311  rexrnmpo  7500  imaeqexov  7598  iunpw  7718  abrexex2g  7910  el2xptp  7981  poxp2  8086  poxp3  8093  soseq  8102  frrlem9  8237  rdglem1  8347  tz7.49  8377  oarec  8490  omeu  8513  qsid  8721  eroveu  8752  ixp0  8872  fimax2g  9189  marypha2lem2  9342  dfsup2  9350  infcllem  9394  dfoi  9419  wemapsolem  9458  zfregcl  9502  zfregclOLD  9503  zfreg  9504  zfregfr  9516  oemapso  9594  brttrcl2  9626  ttrclresv  9629  zfregs2  9645  infenaleph  10004  isinfcard  10005  kmlem7  10070  kmlem13  10076  fin23lem26  10238  dffin1-5  10301  fin12  10326  numth  10385  ac6n  10398  zorn2lem7  10415  zorng  10417  brdom7disj  10444  brdom6disj  10445  uniwun  10654  axgroth5  10738  axgroth4  10746  grothprim  10748  npomex  10910  genpass  10923  elreal  11045  dfinfre  12128  infrenegsup  12130  uzwo  12852  ublbneg  12874  xrinfmss2  13254  4fvwrd4  13593  fsuppmapnn0fiubex  13945  fsuppmapnn0ub  13948  mptnn0fsuppr  13952  hashge2el2dif  14433  cshwsexa  14777  dfrtrclrec2  15011  rexanuz  15299  rexfiuz  15301  clim0  15459  cbvsum  15648  cbvsumv  15649  incexc2  15794  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  fprodle  15952  iprodmul  15959  divalglem10  16362  divalgb  16364  ncoprmlnprm  16689  pythagtriplem2  16779  pythagtriplem19  16795  pythagtrip  16796  pceu  16808  prmreclem6  16883  4sqlem12  16918  cshwshashlem1  17057  cshwshash  17066  imasaddfnlem  17483  isdrs2  18263  chnfi  18591  smndex1mgm  18869  smndex1n0mnd  18874  pmtrprfvalrn  19454  pgpfac1lem5  20047  dvdsrval  20332  opprunit  20348  lsmspsn  21071  lsmelval2  21072  islpidl  21315  pzriprnglem3  21473  pzriprnglem10  21480  mat1dimelbas  22446  mat1dimbas  22447  mdetunilem8  22594  pmatcollpw2lem  22752  tgval2  22931  ntreq0  23052  isclo2  23063  neiptopnei  23107  ist0-3  23320  tgcmp  23376  cmpfi  23383  is1stc2  23417  unisngl  23502  xkobval  23561  txtube  23615  txcmplem1  23616  xkococnlem  23634  eltsms  24108  metrest  24499  iscau3  25255  bcth  25306  pmltpc  25427  itg2i1fseq  25732  itg2cn  25740  plyun0  26172  aaliou3lem9  26327  1cubr  26819  dchrvmasumlema  27477  selbergsb  27552  ostth  27616  noseponlem  27642  nosepon  27643  nolt02o  27673  noinfbnd1lem1  27701  noinfbnd1lem4  27704  cuteq1  27823  elold  27865  made0  27869  lrrecfr  27949  leadds1  27995  addsuniflem  28007  addsasslem1  28009  addsasslem2  28010  mulsrid  28119  mulsuniflem  28155  addsdilem1  28157  addsdilem2  28158  mulsasslem1  28169  mulsasslem2  28170  z12sge0  28489  elreno2  28501  renegscl  28504  istrkg2ld  28542  tglowdim1i  28583  legtrid  28673  midex  28819  ishpg  28841  brbtwn2  28988  colinearalg  28993  ax5seg  29021  axpasch  29024  axlowdimlem6  29030  axeuclidlem  29045  axeuclid  29046  elntg2  29068  umgr2edg1  29294  umgr2edgneu  29297  nbgrsym  29446  isuvtx  29478  usgr2pth0  29848  wlkiswwlksupgr2  29960  clwwlknun  30197  4cycl2vnunb  30375  fusgreg2wsp  30421  lpni  30566  nmobndseqi  30865  hhcmpl  31286  shne0i  31534  nmcopexi  32113  nmcfnexi  32137  cdj3lem3b  32526  rexcom4f  32552  reuxfrdf  32575  iunin1f  32642  ofpreima  32753  intimafv  32799  fpwrelmapffslem  32820  tosglblem  33049  xrnarchi  33260  isunit2  33316  isdrng4  33371  dvdsrspss  33462  lsmsnorb  33466  lsmsnorb2  33467  1arithufdlem4  33622  constrconj  33905  ordtconnlem1  34084  lmdvg  34113  esumfsup  34230  reprsuc  34775  reprdifc  34787  bnj168  34889  bnj1185  34951  bnj1542  35015  bnj865  35081  bnj916  35091  bnj983  35109  bnj1176  35163  bnj1189  35167  bnj1296  35179  bnj1398  35192  bnj1450  35208  bnj1463  35213  nummin  35252  fineqvnttrclse  35284  axregszf  35289  onvf1odlem1  35301  loop1cycl  35335  cvmliftlem15  35496  cvmlift2lem12  35512  satfvsuclem2  35558  satfvsucsuc  35563  satfdm  35567  satf0  35570  dmopab3rexdif  35603  rexxfr3dALT  35837  dffr5  35952  dfon2lem9  35987  brbigcup  36094  elfuns  36111  brimage  36122  brimg  36133  dfrecs2  36148  imagesset  36151  brub  36152  brsegle  36306  sumeq2si  36400  prodeq2si  36402  cbvprodvw2  36445  filnetlem4  36579  bj-rexcom4bv  37205  bj-rexcom4b  37206  bj-elsngl  37291  bj-axseprep  37397  bj-rest10  37416  bj-restreg  37427  bj-mpomptALT  37447  nlpineqsn  37738  fvineqsneq  37742  iundif1  37929  matunitlindflem1  37951  poimirlem1  37956  poimirlem30  37985  poimirlem32  37987  poimir  37988  ismblfin  37996  volsupnfl  38000  itg2addnclem3  38008  fdc  38080  isfldidl  38403  eldmqsres2  38629  n0elqs  38667  rnxrncnvepres  38758  rnxrnidres  38759  dfcoels  38855  br1cossinres  38872  br1cossinidres  38874  br1cossincnvepres  38875  br1cossxrnidres  38876  br1cossxrncnvepres  38877  br1cossxrncnvssrres  38923  eldmqs1cossres  39079  disjdmqscossss  39241  prtlem10  39325  prter2  39341  islshpat  39477  lshpsmreu  39569  2dim  39930  islpln5  39995  lplnexatN  40023  islvol5  40039  dalem18  40141  dalem20  40153  lhpexle2  40470  lhpexle3  40472  lhpex2leN  40473  4atex2  40537  4atex2-0bOLDN  40539  cdlemftr3  41025  cdlemg17pq  41132  cdlemg19  41144  cdlemg21  41146  cdlemg33d  41169  dva1dim  41445  dih1dimatlem  41789  dihglb2  41802  dvh2dim  41905  mapdrvallem2  42105  mapdpglem3  42135  hdmapglem7a  42387  hashnexinjle  42582  aks6d1c5  42592  supinf  42695  fimgmcyclem  42992  dffltz  43081  elrfirn  43141  isnacs2  43152  isnacs3  43156  sbc2rex  43233  4rexfrabdioph  43244  eldioph4b  43257  fphpd  43262  fiphp3d  43265  rencldnfilem  43266  rmxdioph  43462  expdiophlem1  43467  islnm2  43524  onmaxnelsup  43669  onsupnmax  43674  onsupuni  43675  onsupmaxb  43685  tfsconcatlem  43782  tfsconcatrn  43788  oadif1lem  43825  oadif1  43826  elimaint  44094  cnviun  44095  imaiun1  44096  coiun1  44097  elintima  44098  briunov2  44127  clsk3nimkb  44485  expandrexn  44736  prmunb2  44756  zfregs2VD  45285  n0abso  45421  sswfaxreg  45432  evth2f  45464  evthf  45476  ndisj2  45500  rexanuz2nf  45938  fnlimabslt  46125  climbddf  46133  limsupub  46150  limsuppnflem  46156  limsupubuz  46159  limsupre2lem  46170  limsupreuz  46183  limsupvaluz2  46184  cnrefiisplem  46275  cnrefiisp  46276  stoweidlem28  46474  fourierdlem63  46615  fourierdlem65  46617  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem100  46652  sge0pnfmpt  46891  ovn0  47012  smfaddlem1  47209  smflimlem4  47220  fsetsniunop  47509  2rexsb  47561  2rexrsb  47562  cbvrex2  47564  2reu8i  47573  clnbgrsym  48326  isubgr3stgrlem6  48459  copisnmnd  48657  pgrpgt2nabl  48854  islindeps  48941  lindslinindsimp1  48945  lindslinindsimp2  48951  islindeps2  48971  islininds2  48972  isldepslvec2  48973  ldepslinc  48997  sepnsepolem1  49409