Theorem rexbii 3115

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  r19.29imd  3133  r19.43  3136  3r19.43  3137  2rexbii  3144  rexnal2  3150  r19.42v  3200  r19.41vv  3238  3reeanv  3241  cbvrex2vw  3251  rexcom4a  3298  rexcom13  3301  rexrot4  3302  2ex2rexrot  3303  cbvrex2v  3361  rexcom4b  3489  ceqsrex2v  3620  clel5  3627  reu7  3698  2reu5a  3710  0el  4321  n0snor2el  4803  uni0b  4904  iuncom  4969  iuncom4  4970  iuniin  4974  dfiunv2  5003  iunab  5021  iunid  5030  iunsn  5035  iunn0  5036  iunin2  5040  iundif2  5043  iunun  5064  iunxiun  5068  iunpwss  5078  axrep6OLD  5253  inuni  5325  reusv2lem5  5378  iunopab  5549  dffr2  5627  dffr2ALT  5628  frc  5629  frminex  5645  dfepfr  5650  epfrc  5651  xpiundi  5737  xpiundir  5738  reliin  5809  iunxpf  5839  cnvuni  5881  dmiun  5908  dmopab2rex  5912  elres  6024  elidinxp  6051  dfima3  6070  dffr3  6106  rniun  6150  xpdifid  6170  xpdifcnvepel  6171  dminxp  6183  imaco  6257  coiun  6263  imaindm  6307  dffr4  6328  frpomin2  6349  sucel  6444  isarep1  6631  rexrn  7089  ralrn  7090  elrnrexdmb  7092  fnasrn  7148  ralima  7242  reximaOLD  7244  ralimaOLD  7245  abrexco  7249  imaiun  7250  fliftcnv  7320  imaeqsexvOLD  7374  rexrnmpo  7563  imaeqexov  7661  iunpw  7779  abrexex2g  7970  el2xptp  8041  poxp2  8148  poxp3  8155  soseq  8164  frrlem9  8300  rdglem1  8411  tz7.49  8441  oarec  8556  omeu  8579  qsid  8788  eroveu  8819  ixp0  8938  fimax2g  9256  marypha2lem2  9406  dfsup2  9414  infcllem  9458  dfoi  9483  wemapsolem  9522  zfregcl  9566  zfregclOLD  9567  zfreg  9568  zfregfr  9583  oemapso  9661  brttrcl2  9693  ttrclresv  9696  zfregs2  9712  infenaleph  10094  isinfcard  10095  kmlem7  10159  kmlem13  10165  fin23lem26  10327  dffin1-5  10390  fin12  10415  numth  10474  ac6n  10487  zorn2lem7  10504  zorng  10506  brdom7disj  10533  brdom6disj  10534  uniwun  10743  axgroth5  10827  axgroth4  10835  grothprim  10837  npomex  10999  genpass  11012  elreal  11134  dfinfre  12214  infrenegsup  12216  uzwo  12953  ublbneg  12975  xrinfmss2  13355  4fvwrd4  13695  fsuppmapnn0fiubex  14048  fsuppmapnn0ub  14051  mptnn0fsuppr  14055  hashge2el2dif  14537  cshwsexa  14887  dfrtrclrec2  15121  rexanuz  15423  rexfiuz  15425  clim0  15583  cbvsum  15772  cbvsumv  15773  incexc2  15918  cbvprod  15993  cbvprodv  15994  prodeq1i  15996  fprodle  16076  iprodmul  16083  divalglem10  16485  divalgb  16487  ncoprmlnprm  16812  pythagtriplem2  16902  pythagtriplem19  16918  pythagtrip  16919  pceu  16931  prmreclem6  17006  4sqlem12  17041  cshwshashlem1  17180  cshwshash  17189  imasaddfnlem  17607  isdrs2  18387  chnfi  18715  smndex1mgm  19000  smndex1n0mnd  19005  pmtrprfvalrn  19589  pgpfac1lem5  20182  dvdsrval  20476  opprunit  20492  isdrng4  20876  isdrng3lem1  20888  lsmspsn  21242  lsmelval2  21243  islpidl  21530  pzriprnglem3  21670  pzriprnglem10  21677  mat1dimelbas  22665  mat1dimbas  22666  mdetunilem8  22813  pmatcollpw2lem  22971  tgval2  23150  ntreq0  23271  isclo2  23282  neiptopnei  23326  ist0-3  23539  tgcmp  23595  cmpfi  23602  is1stc2  23636  unisngl  23721  xkobval  23780  txtube  23834  txcmplem1  23835  xkococnlem  23853  eltsms  24327  metrest  24718  iscau3  25474  bcth  25525  pmltpc  25646  itg2i1fseq  25951  itg2cn  25959  plyun0  26391  aaliou3lem9  26550  1cubr  27044  dchrvmasumlema  27701  selbergsb  27776  ostth  27840  noseponlem  27865  nosepon  27866  nolt02o  27896  noinfbnd1lem1  27924  noinfbnd1lem4  27927  cuteq1  28047  elold  28089  made0  28093  lrrecfr  28173  leadds1  28219  addsuniflem  28231  addsasslem1  28233  addsasslem2  28234  mulsrid  28343  mulsuniflem  28379  addsdilem1  28381  addsdilem2  28382  mulsasslem1  28393  mulsasslem2  28394  z12sge0  28713  elreno2  28725  renegscl  28728  istrkg2ld  28766  tglowdim1i  28807  legtrid  28897  midex  29055  ishpg  29078  brbtwn2  29292  colinearalg  29297  ax5seg  29325  axpasch  29328  axlowdimlem6  29334  axeuclidlem  29349  axeuclid  29350  elntg2  29372  umgr2edg1  29598  umgr2edgneu  29601  nbgrsym  29750  isuvtx  29782  usgr2pth0  30151  wlkiswwlksupgr2  30263  clwwlknun  30500  4cycl2vnunb  30678  fusgreg2wsp  30724  lpni  30869  nmobndseqi  31168  hhcmpl  31589  shne0i  31837  nmcopexi  32416  nmcfnexi  32440  cdj3lem3b  32829  rexcom4f  32852  reuxfrdf  32874  iunin1f  32939  ofpreima  33047  intimafv  33093  fpwrelmapffslem  33114  tosglblem  33325  xrnarchi  33535  isunit2  33590  dvdsrspss  33731  lsmsnorb  33735  lsmsnorb2  33736  1arithufdlem4  33868  constrconj  34166  ordtconnlem1  34345  lmdvg  34374  esumfsup  34491  reprsuc  35034  reprdifc  35046  bnj168  35151  bnj1185  35213  bnj1542  35277  bnj865  35343  bnj916  35353  bnj983  35371  bnj1176  35425  bnj1189  35429  bnj1296  35441  bnj1398  35454  bnj1450  35470  bnj1463  35475  nummin  35509  fineqvnttrclse  35561  axregszf  35566  onvf1odlem1  35611  loop1cycl  35650  cvmliftlem15  35811  cvmlift2lem12  35827  satfvsuclem2  35873  satfvsucsuc  35878  satfdm  35882  satf0  35885  dmopab3rexdif  35918  rexxfr3dALT  36152  dffr5  36267  dfon2lem9  36302  brbigcup  36409  elfuns  36426  brimage  36437  brimg  36448  dfrecs2  36463  imagesset  36466  brub  36467  brsegle  36621  sumeq2si  36755  prodeq2si  36757  cbvprodvw2  36800  filnetlem4  36933  bj-rexcom4bv  37558  bj-rexcom4b  37559  bj-elsngl  37645  bj-axseprep  37752  bj-rest10  37771  bj-restreg  37782  bj-mpomptALT  37802  nlpineqsn  38095  fvineqsneq  38099  iundif1  38286  matunitlindflem1  38308  poimirlem1  38313  poimirlem30  38342  poimirlem32  38344  poimir  38345  ismblfin  38353  volsupnfl  38357  itg2addnclem3  38365  fdc  38437  isfldidl  38760  eldmqsres2  38984  n0elqs  39022  rnxrncnvepres  39113  rnxrnidres  39114  dfcoels  39210  br1cossinres  39227  br1cossinidres  39229  br1cossincnvepres  39230  br1cossxrnidres  39231  br1cossxrncnvepres  39232  br1cossxrncnvssrres  39278  eldmqs1cossres  39434  disjdmqscossss  39596  prtlem10  39680  prter2  39696  islshpat  39832  lshpsmreu  39924  2dim  40285  islpln5  40350  lplnexatN  40378  islvol5  40394  dalem18  40496  dalem20  40508  lhpexle2  40825  lhpexle3  40827  lhpex2leN  40828  4atex2  40892  4atex2-0bOLDN  40894  cdlemftr3  41380  cdlemg17pq  41487  cdlemg19  41499  cdlemg21  41501  cdlemg33d  41524  dva1dim  41800  dih1dimatlem  42144  dihglb2  42157  dvh2dim  42260  mapdrvallem2  42460  mapdpglem3  42490  hdmapglem7a  42742  hashnexinjle  42937  aks6d1c5  42947  supinf  43051  fimgmcyclem  43342  dffltz  43407  elrfirn  43467  isnacs2  43478  isnacs3  43482  sbc2rex  43557  4rexfrabdioph  43566  eldioph4b  43579  fphpd  43584  fiphp3d  43587  rencldnfilem  43588  rmxdioph  43784  expdiophlem1  43789  islnm2  43846  onmaxnelsup  43991  onsupnmax  43996  onsupuni  43997  onsupmaxb  44007  tfsconcatlem  44104  tfsconcatrn  44110  oadif1lem  44147  oadif1  44148  elimaint  44416  cnviun  44417  imaiun1  44418  coiun1  44419  elintima  44420  briunov2  44449  clsk3nimkb  44807  expandrexn  45042  prmunb2  45062  zfregs2VD  45590  n0abso  45726  sswfaxreg  45737  evth2f  45776  evthf  45788  ndisj2  45812  rexanuz2nf  46247  fnlimabslt  46434  climbddf  46442  limsupub  46459  limsuppnflem  46465  limsupubuz  46468  limsupre2lem  46479  limsupreuz  46492  limsupvaluz2  46493  cnrefiisplem  46584  cnrefiisp  46585  stoweidlem28  46783  fourierdlem63  46924  fourierdlem65  46926  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem100  46961  sge0pnfmpt  47200  ovn0  47321  smfaddlem1  47518  smflimlem4  47529  fsetsniunop  47827  2rexsb  47879  2rexrsb  47880  cbvrex2  47882  2reu8i  47891  clnbgrsym  48644  isubgr3stgrlem6  48777  copisnmnd  48975  pgrpgt2nabl  49187  islindeps  49274  lindslinindsimp1  49278  lindslinindsimp2  49284  islindeps2  49304  islininds2  49305  isldepslvec2  49306  ldepslinc  49330  sepnsepolem1  49741  ralsbii  50620