Theorem rexbii 3084

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

Syntax hints:   ↔ wb 205   ∈ wcel 2099  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061

This theorem is referenced by:  r19.29imd  3108  r19.43  3112  2rexbii  3119  rexnal2  3125  r19.42v  3181  r19.41vv  3215  3reeanv  3218  2ralorOLD  3220  cbvrex2vw  3230  rexcomOLD  3279  rexcom4a  3280  rexcom13  3284  rexrot4  3285  2ex2rexrot  3286  cbvrex2v  3353  rexcom4b  3494  ceqsrex2v  3642  clel5  3651  reu7  3725  2reu5a  3737  0el  4356  n0snor2el  4832  uni0b  4933  iuncom  5000  iuncom4  5001  iuniin  5005  dfiunv2  5035  iunab  5051  iunid  5060  iunsn  5066  iunn0  5067  iunin2  5071  iundif2  5074  iunun  5093  iunxiun  5097  iunpwss  5107  axrep6  5289  inuni  5342  reusv2lem5  5398  iunopab  5557  iunopabOLD  5558  dffr2  5638  dffr2ALT  5639  frc  5640  frminex  5654  dfepfr  5659  epfrc  5660  xpiundi  5744  xpiundir  5745  reliin  5815  iunxpf  5847  cnvuni  5885  dmiun  5912  dmopab2rex  5916  elres  6021  elidinxp  6045  dfima3  6064  dffr3  6101  rniun  6151  xpdifid  6171  dminxp  6183  imaco  6254  coiun  6259  imaindm  6302  dffr4  6324  frpomin2  6346  tz6.26OLD  6353  sucel  6442  isarep1  6640  isarep1OLD  6641  rexrn  7093  ralrn  7094  elrnrexdmb  7096  fnasrn  7151  rexima  7246  ralima  7247  abrexco  7251  imaiun  7252  fliftcnv  7315  imaeqsexv  7367  rexrnmpo  7558  imaeqexov  7656  iunpw  7771  abrexex2g  7970  el2xptp  8041  poxp2  8149  poxp3  8156  soseq  8165  frrlem9  8301  rdglem1  8437  tz7.49  8467  oarec  8584  omeu  8607  qsid  8804  eroveu  8833  ixp0  8952  fimax2g  9316  marypha2lem2  9472  dfsup2  9480  infcllem  9523  dfoi  9547  wemapsolem  9586  zfregcl  9630  zfreg  9631  zfregfr  9641  oemapso  9718  brttrcl2  9750  ttrclresv  9753  zfregs2  9769  infenaleph  10127  isinfcard  10128  kmlem7  10192  kmlem13  10198  fin23lem26  10359  dffin1-5  10422  fin12  10447  numth  10506  ac6n  10519  zorn2lem7  10536  zorng  10538  brdom7disj  10565  brdom6disj  10566  uniwun  10774  axgroth5  10858  axgroth4  10866  grothprim  10868  npomex  11030  genpass  11043  elreal  11165  dfinfre  12241  infrenegsup  12243  uzwo  12941  ublbneg  12963  xrinfmss2  13338  4fvwrd4  13669  fsuppmapnn0fiubex  14006  fsuppmapnn0ub  14009  mptnn0fsuppr  14013  hashge2el2dif  14494  cshwsexa  14827  dfrtrclrec2  15058  rexanuz  15345  rexfiuz  15347  clim0  15503  cbvsum  15694  incexc2  15837  cbvprod  15912  fprodle  15993  iprodmul  16000  divalglem10  16399  divalgb  16401  ncoprmlnprm  16725  pythagtriplem2  16814  pythagtriplem19  16830  pythagtrip  16831  pceu  16843  prmreclem6  16918  4sqlem12  16953  cshwshashlem1  17093  cshwshash  17102  imasaddfnlem  17538  isdrs2  18326  smndex1mgm  18892  smndex1n0mnd  18897  pmtrprfvalrn  19482  pgpfac1lem5  20075  dvdsrval  20339  opprunit  20355  lsmspsn  21058  lsmelval2  21059  islpidl  21310  pzriprnglem3  21469  pzriprnglem10  21476  mat1dimelbas  22461  mat1dimbas  22462  mdetunilem8  22609  pmatcollpw2lem  22767  tgval2  22947  ntreq0  23069  isclo2  23080  neiptopnei  23124  ist0-3  23337  tgcmp  23393  cmpfi  23400  is1stc2  23434  unisngl  23519  xkobval  23578  txtube  23632  txcmplem1  23633  xkococnlem  23651  eltsms  24125  metrest  24521  iscau3  25294  bcth  25345  pmltpc  25467  itg2i1fseq  25773  itg2cn  25781  plyun0  26221  aaliou3lem9  26375  1cubr  26867  dchrvmasumlema  27526  selbergsb  27601  ostth  27665  noseponlem  27691  nosepon  27692  nolt02o  27722  noinfbnd1lem1  27750  noinfbnd1lem4  27753  cuteq1  27860  elold  27890  made0  27894  lrrecfr  27954  sleadd1  28000  addsuniflem  28012  addsasslem1  28014  addsasslem2  28015  mulsrid  28111  mulsuniflem  28147  addsdilem1  28149  addsdilem2  28150  mulsasslem1  28161  mulsasslem2  28162  renegscl  28346  istrkg2ld  28384  tglowdim1i  28425  legtrid  28515  midex  28661  ishpg  28683  brbtwn2  28836  colinearalg  28841  ax5seg  28869  axpasch  28872  axlowdimlem6  28878  axeuclidlem  28893  axeuclid  28894  elntg2  28916  umgr2edg1  29144  umgr2edgneu  29147  nbgrsym  29296  isuvtx  29328  usgr2pth0  29699  wlkiswwlksupgr2  29808  clwwlknun  30042  4cycl2vnunb  30220  fusgreg2wsp  30266  lpni  30410  nmobndseqi  30709  hhcmpl  31130  shne0i  31378  nmcopexi  31957  nmcfnexi  31981  cdj3lem3b  32370  rexcom4f  32395  reuxfrdf  32416  iunin1f  32478  ofpreima  32582  intimafv  32622  fpwrelmapffslem  32646  tosglblem  32847  xrnarchi  33053  isdrng4  33152  dvdsrspss  33268  lsmsnorb  33272  lsmsnorb2  33273  1arithufdlem4  33428  constrconj  33617  ordtconnlem1  33752  lmdvg  33781  esumfsup  33916  reprsuc  34474  reprdifc  34486  bnj168  34588  bnj1185  34651  bnj1542  34715  bnj865  34781  bnj916  34791  bnj983  34809  bnj1176  34863  bnj1189  34867  bnj1296  34879  bnj1398  34892  bnj1450  34908  bnj1463  34913  nummin  34941  loop1cycl  34978  cvmliftlem15  35139  cvmlift2lem12  35155  satfvsuclem2  35201  satfvsucsuc  35206  satfdm  35210  satf0  35213  dmopab3rexdif  35246  rexxfr3dALT  35480  dffr5  35589  dfon2lem9  35628  brbigcup  35735  elfuns  35752  brimage  35763  brimg  35774  dfrecs2  35787  imagesset  35790  brub  35791  brsegle  35945  filnetlem4  36106  bj-rexcom4bv  36601  bj-rexcom4b  36602  bj-elsngl  36688  bj-rest10  36808  bj-restreg  36819  bj-mpomptALT  36839  nlpineqsn  37128  fvineqsneq  37132  iundif1  37308  matunitlindflem1  37330  poimirlem1  37335  poimirlem30  37364  poimirlem32  37366  poimir  37367  ismblfin  37375  volsupnfl  37379  itg2addnclem3  37387  fdc  37459  isfldidl  37782  eldmqsres2  37999  n0elqs  38037  rnxrncnvepres  38111  rnxrnidres  38112  dfcoels  38141  br1cossinres  38158  br1cossinidres  38160  br1cossincnvepres  38161  br1cossxrnidres  38162  br1cossxrncnvepres  38163  br1cossxrncnvssrres  38219  eldmqs1cossres  38370  disjdmqscossss  38514  prtlem10  38576  prter2  38592  islshpat  38728  lshpsmreu  38820  2dim  39182  islpln5  39247  lplnexatN  39275  islvol5  39291  dalem18  39393  dalem20  39405  lhpexle2  39722  lhpexle3  39724  lhpex2leN  39725  4atex2  39789  4atex2-0bOLDN  39791  cdlemftr3  40277  cdlemg17pq  40384  cdlemg19  40396  cdlemg21  40398  cdlemg33d  40421  dva1dim  40697  dih1dimatlem  41041  dihglb2  41054  dvh2dim  41157  mapdrvallem2  41357  mapdpglem3  41387  hdmapglem7a  41639  hashnexinjle  41841  aks6d1c5  41851  supinf  41988  fimgmcyclem  42223  dffltz  42324  elrfirn  42389  isnacs2  42400  isnacs3  42404  sbc2rex  42481  4rexfrabdioph  42492  eldioph4b  42505  fphpd  42510  fiphp3d  42513  rencldnfilem  42514  rmxdioph  42711  expdiophlem1  42716  islnm2  42776  onmaxnelsup  42925  onsupnmax  42930  onsupuni  42931  onsupmaxb  42941  tfsconcatlem  43039  tfsconcatrn  43045  oadif1lem  43082  oadif1  43083  elimaint  43353  cnviun  43354  imaiun1  43355  coiun1  43356  elintima  43357  briunov2  43386  clsk3nimkb  43744  expandrexn  44002  prmunb2  44022  zfregs2VD  44554  evth2f  44651  evthf  44663  ndisj2  44689  rexanuz2nf  45144  fnlimabslt  45336  climbddf  45344  limsupub  45361  limsuppnflem  45367  limsupubuz  45370  limsupre2lem  45381  limsupreuz  45394  limsupvaluz2  45395  cnrefiisplem  45486  cnrefiisp  45487  stoweidlem28  45685  fourierdlem63  45826  fourierdlem65  45828  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem100  45863  sge0pnfmpt  46102  ovn0  46223  smfaddlem1  46420  smflimlem4  46431  fsetsniunop  46700  2rexsb  46750  2rexrsb  46751  cbvrex2  46753  2reu8i  46762  clnbgrsym  47444  copisnmnd  47582  pgrpgt2nabl  47781  islindeps  47872  lindslinindsimp1  47876  lindslinindsimp2  47882  islindeps2  47902  islininds2  47903  isldepslvec2  47904  ldepslinc  47928  sepnsepolem1  48291