Theorem rexbii 3111

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∃wrex 3088

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 3089

This theorem is used by:  r19.29imd  3129  r19.43  3132  3r19.43  3133  2rexbii  3140  rexnal2  3146  r19.42v  3196  r19.41vv  3234  3reeanv  3237  cbvrex2vw  3247  rexcom4a  3294  rexcom13  3297  rexrot4  3298  2ex2rexrot  3299  cbvrex2v  3356  rexcom4b  3484  ceqsrex2v  3615  clel5  3622  reu7  3693  2reu5a  3705  0el  4314  n0snor2el  4796  uni0b  4897  iuncom  4962  iuncom4  4963  iuniin  4967  dfiunv2  4996  iunab  5014  iunid  5023  iunsn  5028  iunn0  5029  iunin2  5033  iundif2  5036  iunun  5057  iunxiun  5061  iunpwss  5071  axrep6OLD  5246  inuni  5318  reusv2lem5  5371  iunopab  5542  dffr2  5620  dffr2ALT  5621  frc  5622  frminex  5638  dfepfr  5643  epfrc  5644  xpiundi  5730  xpiundir  5731  reliin  5802  iunxpf  5832  cnvuni  5874  dmiun  5901  dmopab2rex  5905  elres  6017  elidinxp  6044  dfima3  6063  dffr3  6099  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  dminxp  6177  imaco  6251  coiun  6257  imaindm  6301  dffr4  6322  frpomin2  6343  sucel  6438  isarep1  6625  rexrn  7084  ralrn  7085  elrnrexdmb  7087  fnasrn  7145  ralima  7240  abrexco  7245  imaiun  7246  fliftcnv  7316  rexrnmpo  7557  imaeqexov  7656  iunpw  7774  abrexex2g  7965  el2xptp  8036  poxp2  8145  poxp3  8152  soseq  8161  frrlem9  8297  rdglem1  8408  tz7.49  8438  oarec  8553  omeu  8576  qsid  8785  eroveu  8816  ixp0  8942  fimax2g  9260  marypha2lem2  9410  dfsup2  9418  infcllem  9462  dfoi  9487  wemapsolem  9526  zfregcl  9570  zfregclOLD  9571  zfreg  9572  zfregfr  9587  oemapso  9665  brttrcl2  9697  ttrclresv  9700  zfregs2  9716  infenaleph  10098  isinfcard  10099  kmlem7  10163  kmlem13  10169  fin23lem26  10331  dffin1-5  10394  fin12  10419  numth  10478  ac6n  10491  zorn2lem7  10508  zorng  10510  brdom7disj  10538  brdom6disj  10539  uniwun  10753  axgroth5  10837  axgroth4  10845  grothprim  10847  npomex  11009  genpass  11022  elreal  11144  dfinfre  12224  infrenegsup  12226  uzwo  12964  ublbneg  12986  xrinfmss2  13367  4fvwrd4  13707  fsuppmapnn0fiubex  14060  fsuppmapnn0ub  14063  mptnn0fsuppr  14067  hashge2el2dif  14549  cshwsexa  14899  dfrtrclrec2  15135  rexanuz  15437  rexfiuz  15439  clim0  15597  cbvsum  15786  cbvsumv  15787  incexc2  15931  cbvprod  16006  cbvprodv  16007  prodeq1i  16009  fprodle  16089  iprodmul  16096  divalglem10  16498  divalgb  16500  ncoprmlnprm  16825  pythagtriplem2  16915  pythagtriplem19  16931  pythagtrip  16932  pceu  16944  prmreclem6  17019  4sqlem12  17054  cshwshashlem1  17193  cshwshash  17202  imasaddfnlem  17620  isdrs2  18400  chnfi  18728  smndex1mgm  19025  smndex1n0mnd  19030  pmtrprfvalrn  19621  pgpfac1lem5  20214  dvdsrval  20508  opprunit  20524  isdrng4  20908  isdrng3lem1  20920  lsmspsn  21274  lsmelval2  21275  islpidl  21562  pzriprnglem3  21702  pzriprnglem10  21709  mat1dimelbas  22699  mat1dimbas  22700  mdetunilem8  22847  matunitlindflem1  22907  pmatcollpw2lem  23008  tgval2  23187  ntreq0  23308  isclo2  23319  neiptopnei  23363  ist0-3  23576  tgcmp  23632  cmpfi  23639  is1stc2  23673  unisngl  23759  xkobval  23818  txtube  23872  txcmplem1  23873  xkococnlem  23891  eltsms  24365  metrest  24756  iscau3  25512  bcth  25563  pmltpc  25684  itg2i1fseq  25989  itg2cn  25997  plyun0  26429  plyconz  26547  aaliou3lem9  26593  1cubr  27087  dchrvmasumlema  27744  selbergsb  27819  ostth  27883  noseponlem  27908  nosepon  27909  nolt02o  27939  noinfbnd1lem1  27967  noinfbnd1lem4  27970  cuteq1  28090  elold  28132  made0  28136  lrrecfr  28216  leadds1  28262  addsuniflem  28274  addsasslem1  28276  addsasslem2  28277  mulsrid  28386  mulsuniflem  28422  addsdilem1  28424  addsdilem2  28425  mulsasslem1  28436  mulsasslem2  28437  z12sge0  28756  elreno2  28768  renegscl  28771  istrkg2ld  28809  tglowdim1i  28851  legtrid  28941  midex  29100  ishpg  29124  brbtwn2  29370  colinearalg  29375  ax5seg  29403  axpasch  29406  axlowdimlem6  29412  axeuclidlem  29427  axeuclid  29428  elntg2  29450  umgr2edg1  29679  umgr2edgneu  29682  nbgrsym  29831  isuvtx  29863  usgr2pth0  30238  wlkiswwlksupgr2  30353  clwwlknun  30590  loop1cycl  30631  4cycl2vnunb  30778  fusgreg2wsp  30824  lpni  30969  nmobndseqi  31268  hhcmpl  31689  shne0i  31937  nmcopexi  32516  nmcfnexi  32540  cdj3lem3b  32929  rexcom4f  32952  reuxfrdf  32974  iunin1f  33039  ofpreima  33146  intimafv  33191  fpwrelmapffslem  33211  tosglblem  33422  xrnarchi  33632  isunit2  33687  dvdsrspss  33828  lsmsnorb  33832  lsmsnorb2  33833  1arithufdlem4  33965  constrconj  34263  ordtconnlem1  34442  lmdvg  34471  esumfsup  34588  reprsuc  35131  reprdifc  35143  bnj168  35248  bnj1185  35310  bnj1542  35374  bnj865  35440  bnj916  35450  bnj983  35468  bnj1176  35522  bnj1189  35526  bnj1296  35538  bnj1398  35551  bnj1450  35567  bnj1463  35572  nummin  35606  fineqvnttrclse  35658  axregszf  35663  onvf1odlem1  35708  cvmliftlem15  35885  cvmlift2lem12  35901  satfvsuclem2  35947  satfvsucsuc  35952  satfdm  35956  satf0  35959  dmopab3rexdif  35992  rexxfr3dALT  36226  dffr5  36341  dfon2lem9  36376  brbigcup  36483  elfuns  36500  brimage  36511  brimg  36522  dfrecs2  36537  imagesset  36540  brub  36541  dffr7  36543  brsegle  36696  sumeq2si  36830  prodeq2si  36832  cbvprodvw2  36875  filnetlem4  37008  bj-rexcom4bv  37633  bj-rexcom4b  37634  bj-elsngl  37720  bj-axseprep  37827  bj-rest10  37846  bj-restreg  37857  bj-mpomptALT  37877  nlpineqsn  38170  fvineqsneq  38174  iundif1  38361  poimirlem1  38378  poimirlem30  38407  poimirlem32  38409  poimir  38410  ismblfin  38418  volsupnfl  38422  itg2addnclem3  38430  fdc  38503  isfldidl  38826  eldmqsres2  39050  n0elqs  39088  rnxrncnvepres  39179  rnxrnidres  39180  dfcoels  39276  br1cossinres  39293  br1cossinidres  39295  br1cossincnvepres  39296  br1cossxrnidres  39297  br1cossxrncnvepres  39298  br1cossxrncnvssrres  39344  eldmqs1cossres  39500  disjdmqscossss  39662  prtlem10  39746  prter2  39762  islshpat  39898  lshpsmreu  39990  2dim  40351  islpln5  40416  lplnexatN  40444  islvol5  40460  dalem18  40562  dalem20  40574  lhpexle2  40891  lhpexle3  40893  lhpex2leN  40894  4atex2  40958  4atex2-0bOLDN  40960  cdlemftr3  41446  cdlemg17pq  41553  cdlemg19  41565  cdlemg21  41567  cdlemg33d  41590  dva1dim  41866  dih1dimatlem  42210  dihglb2  42223  dvh2dim  42326  mapdrvallem2  42526  mapdpglem3  42556  hdmapglem7a  42808  hashnexinjle  43003  aks6d1c5  43013  supinf  43117  fimgmcyclem  43423  dffltz  43488  elrfirn  43548  isnacs2  43559  isnacs3  43563  sbc2rex  43638  4rexfrabdioph  43647  eldioph4b  43660  fphpd  43665  fiphp3d  43668  rencldnfilem  43669  rmxdioph  43865  expdiophlem1  43870  islnm2  43927  onmaxnelsup  44072  onsupnmax  44077  onsupuni  44078  onsupmaxb  44088  tfsconcatlem  44185  tfsconcatrn  44191  oadif1lem  44228  oadif1  44229  elimaint  44497  cnviun  44498  imaiun1  44499  coiun1  44500  elintima  44501  briunov2  44530  clsk3nimkb  44888  expandrexn  45123  prmunb2  45143  zfregs2VD  45671  n0abso  45807  sswfaxreg  45818  evth2f  45857  evthf  45869  ndisj2  45893  rexanuz2nf  46328  fnlimabslt  46515  climbddf  46523  limsupub  46540  limsuppnflem  46546  limsupubuz  46549  limsupre2lem  46560  limsupreuz  46573  limsupvaluz2  46574  cnrefiisplem  46665  cnrefiisp  46666  stoweidlem28  46864  fourierdlem63  47005  fourierdlem65  47007  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem100  47042  sge0pnfmpt  47281  ovn0  47402  smfaddlem1  47599  smflimlem4  47610  fsetsniunop  47945  2rexsb  47997  2rexrsb  47998  cbvrex2  48000  2reu8i  48009  clnbgrsym  48762  isubgr3stgrlem6  48895  copisnmnd  49092  pgrpgt2nabl  49304  islindeps  49391  lindslinindsimp1  49395  lindslinindsimp2  49401  islindeps2  49421  islininds2  49422  isldepslvec2  49423  ldepslinc  49447  sepnsepolem1  49856  ralsbii  50738