Theorem rexbii 3079

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  r19.29imd  3097  r19.43  3100  3r19.43  3101  2rexbii  3108  rexnal2  3114  r19.42v  3164  r19.41vv  3202  3reeanv  3205  cbvrex2vw  3215  rexcom4a  3262  rexcom13  3265  rexrot4  3266  2ex2rexrot  3267  cbvrex2v  3335  rexcom4b  3468  ceqsrex2v  3613  clel5  3620  reu7  3691  2reu5a  3703  0el  4313  n0snor2el  4785  uni0b  4885  iuncom  4949  iuncom4  4950  iuniin  4954  dfiunv2  4984  iunab  5000  iunid  5009  iunsn  5014  iunn0  5015  iunin2  5019  iundif2  5022  iunun  5041  iunxiun  5045  iunpwss  5055  axrep6OLD  5227  inuni  5288  reusv2lem5  5340  iunopab  5499  dffr2  5577  dffr2ALT  5578  frc  5579  frminex  5595  dfepfr  5600  epfrc  5601  xpiundi  5687  xpiundir  5688  reliin  5757  iunxpf  5788  cnvuni  5826  dmiun  5853  dmopab2rex  5857  elres  5969  elidinxp  5993  dfima3  6012  dffr3  6048  rniun  6094  xpdifid  6115  dminxp  6127  imaco  6198  coiun  6204  imaindm  6246  dffr4  6267  frpomin2  6288  sucel  6382  isarep1  6570  rexrn  7020  ralrn  7021  elrnrexdmb  7023  fnasrn  7078  ralima  7171  reximaOLD  7173  ralimaOLD  7174  abrexco  7178  imaiun  7179  fliftcnv  7245  imaeqsexvOLD  7297  rexrnmpo  7486  imaeqexov  7584  iunpw  7704  abrexex2g  7896  el2xptp  7967  poxp2  8073  poxp3  8080  soseq  8089  frrlem9  8224  rdglem1  8334  tz7.49  8364  oarec  8477  omeu  8500  qsid  8705  eroveu  8736  ixp0  8855  fimax2g  9170  marypha2lem2  9320  dfsup2  9328  infcllem  9372  dfoi  9397  wemapsolem  9436  zfregcl  9480  zfregclOLD  9481  zfreg  9482  zfregfr  9494  oemapso  9572  brttrcl2  9604  ttrclresv  9607  zfregs2  9623  infenaleph  9979  isinfcard  9980  kmlem7  10045  kmlem13  10051  fin23lem26  10213  dffin1-5  10276  fin12  10301  numth  10360  ac6n  10373  zorn2lem7  10390  zorng  10392  brdom7disj  10419  brdom6disj  10420  uniwun  10628  axgroth5  10712  axgroth4  10720  grothprim  10722  npomex  10884  genpass  10897  elreal  11019  dfinfre  12100  infrenegsup  12102  uzwo  12806  ublbneg  12828  xrinfmss2  13207  4fvwrd4  13545  fsuppmapnn0fiubex  13896  fsuppmapnn0ub  13899  mptnn0fsuppr  13903  hashge2el2dif  14384  cshwsexa  14728  dfrtrclrec2  14962  rexanuz  15250  rexfiuz  15252  clim0  15410  cbvsum  15599  cbvsumv  15600  incexc2  15742  cbvprod  15817  cbvprodv  15818  prodeq1i  15820  fprodle  15900  iprodmul  15907  divalglem10  16310  divalgb  16312  ncoprmlnprm  16636  pythagtriplem2  16726  pythagtriplem19  16742  pythagtrip  16743  pceu  16755  prmreclem6  16830  4sqlem12  16865  cshwshashlem1  17004  cshwshash  17013  imasaddfnlem  17429  isdrs2  18209  chnfi  18537  smndex1mgm  18812  smndex1n0mnd  18817  pmtrprfvalrn  19398  pgpfac1lem5  19991  dvdsrval  20277  opprunit  20293  lsmspsn  21016  lsmelval2  21017  islpidl  21260  pzriprnglem3  21418  pzriprnglem10  21425  mat1dimelbas  22384  mat1dimbas  22385  mdetunilem8  22532  pmatcollpw2lem  22690  tgval2  22869  ntreq0  22990  isclo2  23001  neiptopnei  23045  ist0-3  23258  tgcmp  23314  cmpfi  23321  is1stc2  23355  unisngl  23440  xkobval  23499  txtube  23553  txcmplem1  23554  xkococnlem  23572  eltsms  24046  metrest  24437  iscau3  25203  bcth  25254  pmltpc  25376  itg2i1fseq  25681  itg2cn  25689  plyun0  26127  aaliou3lem9  26283  1cubr  26777  dchrvmasumlema  27436  selbergsb  27511  ostth  27575  noseponlem  27601  nosepon  27602  nolt02o  27632  noinfbnd1lem1  27660  noinfbnd1lem4  27663  cuteq1  27776  elold  27812  made0  27816  lrrecfr  27884  sleadd1  27930  addsuniflem  27942  addsasslem1  27944  addsasslem2  27945  mulsrid  28050  mulsuniflem  28086  addsdilem1  28088  addsdilem2  28089  mulsasslem1  28100  mulsasslem2  28101  zs12ge0  28391  renegscl  28398  istrkg2ld  28436  tglowdim1i  28477  legtrid  28567  midex  28713  ishpg  28735  brbtwn2  28881  colinearalg  28886  ax5seg  28914  axpasch  28917  axlowdimlem6  28923  axeuclidlem  28938  axeuclid  28939  elntg2  28961  umgr2edg1  29187  umgr2edgneu  29190  nbgrsym  29339  isuvtx  29371  usgr2pth0  29741  wlkiswwlksupgr2  29853  clwwlknun  30087  4cycl2vnunb  30265  fusgreg2wsp  30311  lpni  30455  nmobndseqi  30754  hhcmpl  31175  shne0i  31423  nmcopexi  32002  nmcfnexi  32026  cdj3lem3b  32415  rexcom4f  32442  reuxfrdf  32465  iunin1f  32532  ofpreima  32642  intimafv  32687  fpwrelmapffslem  32710  tosglblem  32950  xrnarchi  33148  isunit2  33202  isdrng4  33256  dvdsrspss  33347  lsmsnorb  33351  lsmsnorb2  33352  1arithufdlem4  33507  constrconj  33753  ordtconnlem1  33932  lmdvg  33961  esumfsup  34078  reprsuc  34623  reprdifc  34635  bnj168  34737  bnj1185  34800  bnj1542  34864  bnj865  34930  bnj916  34940  bnj983  34958  bnj1176  35012  bnj1189  35016  bnj1296  35028  bnj1398  35041  bnj1450  35057  bnj1463  35062  nummin  35099  axregszf  35115  fineqvnttrclse  35132  onvf1odlem1  35135  loop1cycl  35169  cvmliftlem15  35330  cvmlift2lem12  35346  satfvsuclem2  35392  satfvsucsuc  35397  satfdm  35401  satf0  35404  dmopab3rexdif  35437  rexxfr3dALT  35671  dffr5  35786  dfon2lem9  35824  brbigcup  35931  elfuns  35948  brimage  35959  brimg  35970  dfrecs2  35983  imagesset  35986  brub  35987  brsegle  36141  sumeq2si  36235  prodeq2si  36237  cbvprodvw2  36280  filnetlem4  36414  bj-rexcom4bv  36915  bj-rexcom4b  36916  bj-elsngl  37001  bj-rest10  37121  bj-restreg  37132  bj-mpomptALT  37152  nlpineqsn  37441  fvineqsneq  37445  iundif1  37633  matunitlindflem1  37655  poimirlem1  37660  poimirlem30  37689  poimirlem32  37691  poimir  37692  ismblfin  37700  volsupnfl  37704  itg2addnclem3  37712  fdc  37784  isfldidl  38107  eldmqsres2  38321  n0elqs  38359  rnxrncnvepres  38431  rnxrnidres  38432  dfcoels  38466  br1cossinres  38483  br1cossinidres  38485  br1cossincnvepres  38486  br1cossxrnidres  38487  br1cossxrncnvepres  38488  br1cossxrncnvssrres  38544  eldmqs1cossres  38696  disjdmqscossss  38840  prtlem10  38903  prter2  38919  islshpat  39055  lshpsmreu  39147  2dim  39508  islpln5  39573  lplnexatN  39601  islvol5  39617  dalem18  39719  dalem20  39731  lhpexle2  40048  lhpexle3  40050  lhpex2leN  40051  4atex2  40115  4atex2-0bOLDN  40117  cdlemftr3  40603  cdlemg17pq  40710  cdlemg19  40722  cdlemg21  40724  cdlemg33d  40747  dva1dim  41023  dih1dimatlem  41367  dihglb2  41380  dvh2dim  41483  mapdrvallem2  41683  mapdpglem3  41713  hdmapglem7a  41965  hashnexinjle  42161  aks6d1c5  42171  supinf  42274  fimgmcyclem  42565  dffltz  42666  elrfirn  42727  isnacs2  42738  isnacs3  42742  sbc2rex  42819  4rexfrabdioph  42830  eldioph4b  42843  fphpd  42848  fiphp3d  42851  rencldnfilem  42852  rmxdioph  43048  expdiophlem1  43053  islnm2  43110  onmaxnelsup  43255  onsupnmax  43260  onsupuni  43261  onsupmaxb  43271  tfsconcatlem  43368  tfsconcatrn  43374  oadif1lem  43411  oadif1  43412  elimaint  43681  cnviun  43682  imaiun1  43683  coiun1  43684  elintima  43685  briunov2  43714  clsk3nimkb  44072  expandrexn  44323  prmunb2  44343  zfregs2VD  44872  n0abso  45008  sswfaxreg  45019  evth2f  45051  evthf  45063  ndisj2  45087  rexanuz2nf  45529  fnlimabslt  45716  climbddf  45724  limsupub  45741  limsuppnflem  45747  limsupubuz  45750  limsupre2lem  45761  limsupreuz  45774  limsupvaluz2  45775  cnrefiisplem  45866  cnrefiisp  45867  stoweidlem28  46065  fourierdlem63  46206  fourierdlem65  46208  fourierdlem89  46232  fourierdlem90  46233  fourierdlem91  46234  fourierdlem100  46243  sge0pnfmpt  46482  ovn0  46603  smfaddlem1  46800  smflimlem4  46811  fsetsniunop  47079  2rexsb  47131  2rexrsb  47132  cbvrex2  47134  2reu8i  47143  clnbgrsym  47868  isubgr3stgrlem6  48001  copisnmnd  48199  pgrpgt2nabl  48396  islindeps  48484  lindslinindsimp1  48488  lindslinindsimp2  48494  islindeps2  48514  islininds2  48515  isldepslvec2  48516  ldepslinc  48540  sepnsepolem1  48952