Theorem rexbii 3110

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

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

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 3088

This theorem is used by:  r19.29imd  3128  r19.43  3131  3r19.43  3132  2rexbii  3139  rexnal2  3145  r19.42v  3195  r19.41vv  3233  3reeanv  3236  cbvrex2vw  3246  rexcom4a  3293  rexcom13  3296  rexrot4  3297  2ex2rexrot  3298  cbvrex2v  3355  rexcom4b  3482  ceqsrex2v  3612  clel5  3619  reu7  3690  2reu5a  3702  0el  4311  n0snor2el  4793  uni0b  4894  iuncom  4959  iuncom4  4960  iuniin  4964  dfiunv2  4992  iunab  5010  iunid  5019  iunsn  5024  iunn0  5025  iunin2  5029  iundif2  5032  iunun  5053  iunxiun  5057  iunpwss  5067  inuni  5311  reusv2lem5  5364  iunopab  5534  dffr2  5612  dffr2ALT  5613  frc  5614  frminex  5630  dfepfr  5635  epfrc  5636  xpiundi  5722  xpiundir  5723  reliin  5795  el2xptp  5820  iunxpf  5826  cnvuni  5868  dmiun  5895  dmopab2rex  5899  elres  6011  elidinxp  6038  dfima3  6057  dffr3  6093  rniun  6137  xpdifid  6158  xpdifcnvepel  6159  dminxp  6171  imaco  6245  coiun  6251  imaindm  6295  dffr4  6316  frpomin2  6337  sucel  6432  isarep1  6620  rexrn  7079  ralrn  7080  elrnrexdmb  7082  fnasrn  7140  ralima  7235  abrexco  7240  imaiun  7241  fliftcnv  7311  rexrnmpo  7552  imaeqexov  7651  mpt3mpt  7677  iunpw  7774  abrexex2g  7965  poxp2  8144  poxp3  8151  soseq  8160  frrlem9  8296  rdglem1  8407  tz7.49  8439  oarec  8554  omeu  8577  qsid  8786  eroveu  8817  ixp0  8943  fimax2g  9261  marypha2lem2  9412  dfsup2  9420  infcllem  9464  dfoi  9489  wemapsolem  9528  zfregcl  9572  zfregclOLD  9573  zfreg  9574  zfregfr  9589  oemapso  9667  brttrcl2  9699  ttrclresv  9702  zfregs2  9718  infenaleph  10151  isinfcard  10152  kmlem7  10216  kmlem13  10222  fin23lem26  10384  dffin1-5  10447  fin12  10472  numth  10531  ac6n  10544  zorn2lem7  10561  zorng  10563  brdom7disj  10591  brdom6disj  10592  uniwun  10806  axgroth5  10890  axgroth4  10898  grothprim  10900  npomex  11062  genpass  11075  elreal  11197  dfinfre  12279  infrenegsup  12281  uzwo  13019  ublbneg  13041  xrinfmss2  13422  4fvwrd4  13762  fsuppmapnn0fiubex  14115  fsuppmapnn0ub  14118  mptnn0fsuppr  14122  hashge2el2dif  14605  cshwsexa  14955  dfrtrclrec2  15191  rexanuz  15493  rexfiuz  15495  clim0  15653  cbvsum  15842  cbvsumv  15843  incexc2  15987  cbvprod  16062  cbvprodv  16063  prodeq1i  16065  fprodle  16143  iprodmul  16150  divalglem10  16552  divalgb  16554  ncoprmlnprm  16884  pythagtriplem2  16975  pythagtriplem19  16991  pythagtrip  16992  pceu  17004  prmreclem6  17079  4sqlem12  17114  cshwshashlem1  17253  cshwshash  17262  imasaddfnlem  17680  isdrs2  18460  chnfi  18788  smndex1mgm  19086  smndex1n0mnd  19091  pmtrprfvalrn  19682  pgpfac1lem5  20275  dvdsrval  20571  opprunit  20587  isdrng4  20972  isdrng3lem1  20985  lsmspsn  21339  lsmelval2  21340  islpidl  21629  pzriprnglem3  21769  pzriprnglem10  21776  mat1dimelbas  22766  mat1dimbas  22767  mdetunilem8  22914  matunitlindflem1  22974  pmatcollpw2lem  23075  tgval2  23254  ntreq0  23375  isclo2  23386  neiptopnei  23430  ist0-3  23643  tgcmp  23699  cmpfi  23706  is1stc2  23740  unisngl  23826  xkobval  23885  txtube  23939  txcmplem1  23940  xkococnlem  23958  eltsms  24432  metrest  24823  iscau3  25579  bcth  25630  pmltpc  25751  itg2i1fseq  26056  itg2cn  26064  plyun0  26495  plyconz  26613  aaliou3lem9  26659  1cubr  27152  dchrvmasumlema  27809  selbergsb  27884  ostth  27948  noseponlem  28003  nosepon  28004  nolt02o  28034  noinfbnd1lem1  28062  noinfbnd1lem4  28065  cuteq1  28185  elold  28227  made0  28231  lrrecfr  28311  leadds1  28357  addsuniflem  28369  addsasslem1  28371  addsasslem2  28372  mulsrid  28481  mulsuniflem  28517  addsdilem1  28519  addsdilem2  28520  mulsasslem1  28531  mulsasslem2  28532  z12sge0  28851  elreno2  28863  renegscl  28866  istrkg2ld  28904  tglowdim1i  28946  legtrid  29036  midex  29195  ishpg  29219  brbtwn2  29465  colinearalg  29470  ax5seg  29498  axpasch  29501  axlowdimlem6  29507  axeuclidlem  29522  axeuclid  29523  elntg2  29545  umgr2edg1  29774  umgr2edgneu  29777  nbgrsym  29926  isuvtx  29958  usgr2pth0  30333  wlkiswwlksupgr2  30448  clwwlknun  30685  loop1cycl  30726  4cycl2vnunb  30873  fusgreg2wsp  30919  lpni  31064  nmobndseqi  31363  hhcmpl  31784  shne0i  32032  nmcopexi  32611  nmcfnexi  32635  cdj3lem3b  33024  rexcom4f  33047  reuxfrdf  33069  iunin1f  33134  ofpreima  33241  intimafv  33286  fpwrelmapffslem  33306  tosglblem  33517  xrnarchi  33727  isunit2  33782  dvdsrspss  33924  lsmsnorb  33928  lsmsnorb2  33929  1arithufdlem4  34061  constrconj  34359  ordtconnlem1  34538  lmdvg  34567  esumfsup  34684  reprsuc  35227  reprdifc  35239  bnj168  35344  bnj1185  35406  bnj1542  35470  bnj865  35536  bnj916  35546  bnj983  35564  bnj1176  35618  bnj1189  35622  bnj1296  35634  bnj1398  35647  bnj1450  35663  bnj1463  35668  nummin  35701  fineqvnttrclse  35765  axregszf  35770  onvf1odlem1  35855  cvmliftlem15  36032  cvmlift2lem12  36048  satfvsuclem2  36094  satfvsucsuc  36099  satfdm  36103  satf0  36106  dmopab3rexdif  36139  rexxfr3dALT  36373  dffr5  36488  dfon2lem9  36523  brbigcup  36630  elfuns  36647  brimage  36658  brimg  36669  dfrecs2  36684  imagesset  36687  brub  36688  dffr7  36690  brsegle  36843  sumeq2si  36961  prodeq2si  36963  cbvprodvw2  37006  filnetlem4  37139  bj-rexcom4bv  37764  bj-rexcom4b  37765  bj-elsngl  37851  bj-axseprep  37958  bj-rest10  37977  bj-restreg  37988  bj-mpomptALT  38008  nlpineqsn  38299  fvineqsneq  38303  iundif1  38490  poimirlem1  38507  poimirlem30  38536  poimirlem32  38538  poimir  38539  ismblfin  38547  volsupnfl  38551  itg2addnclem3  38559  dfproplem  38609  fdc  38647  isfldidl  38970  eldmqsres2  39194  n0elqs  39232  rnxrncnvepres  39323  rnxrnidres  39324  dfcoels  39420  br1cossinres  39437  br1cossinidres  39439  br1cossincnvepres  39440  br1cossxrnidres  39441  br1cossxrncnvepres  39442  br1cossxrncnvssrres  39488  eldmqs1cossres  39644  disjdmqscossss  39806  prtlem10  39890  prter2  39906  islshpat  40042  lshpsmreu  40134  2dim  40495  islpln5  40560  lplnexatN  40588  islvol5  40604  dalem18  40706  dalem20  40718  lhpexle2  41035  lhpexle3  41037  lhpex2leN  41038  4atex2  41102  4atex2-0bOLDN  41104  cdlemftr3  41590  cdlemg17pq  41697  cdlemg19  41709  cdlemg21  41711  cdlemg33d  41734  dva1dim  42010  dih1dimatlem  42354  dihglb2  42367  dvh2dim  42470  mapdrvallem2  42670  mapdpglem3  42700  hdmapglem7a  42952  hashnexinjle  43147  aks6d1c5  43157  supinf  43261  fimgmcyclem  43559  dffltz  43624  elrfirn  43659  isnacs2  43670  isnacs3  43674  sbc2rex  43749  4rexfrabdioph  43758  eldioph4b  43771  fphpd  43776  fiphp3d  43779  rencldnfilem  43780  rmxdioph  43976  expdiophlem1  43981  islnm2  44038  onmaxnelsup  44183  onsupnmax  44188  onsupuni  44189  onsupmaxb  44199  tfsconcatlem  44296  tfsconcatrn  44302  oadif1lem  44339  oadif1  44340  elimaint  44608  cnviun  44609  imaiun1  44610  coiun1  44611  elintima  44612  briunov2  44641  clsk3nimkb  44999  expandrexn  45234  prmunb2  45254  zfregs2VD  45782  n0abso  45918  sswfaxreg  45929  evth2f  45975  evthf  45987  ndisj2  46011  rexanuz2nf  46446  fnlimabslt  46633  climbddf  46641  limsupub  46658  limsuppnflem  46664  limsupubuz  46667  limsupre2lem  46678  limsupreuz  46691  limsupvaluz2  46692  cnrefiisplem  46783  cnrefiisp  46784  stoweidlem28  46982  fourierdlem63  47123  fourierdlem65  47125  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem100  47160  sge0pnfmpt  47399  ovn0  47520  smfaddlem1  47717  smflimlem4  47728  fsetsniunop  48063  2rexsb  48115  2rexrsb  48116  cbvrex2  48118  2reu8i  48127  clnbgrsym  48880  isubgr3stgrlem6  49013  copisnmnd  49210  pgrpgt2nabl  49422  islindeps  49509  lindslinindsimp1  49513  lindslinindsimp2  49519  islindeps2  49539  islininds2  49540  isldepslvec2  49541  ldepslinc  49565  sepnsepolem1  49974  ralsbii  50841