Theorem rexbii 3210

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	anbi2i 625	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3208	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  2rexbii  3211  2ex2rexrot  3213  rexcom4a  3214  r19.29imd  3218  rexnal2  3219  r19.41vv  3302  r19.42v  3303  r19.43  3304  rexcom  3308  rexcom13  3313  rexrot4  3315  3reeanv  3321  2ralor  3322  cbvrex2vw  3409  cbvrex2v  3412  rexcom4b  3471  rexcom4OLD  3473  ceqsrex2v  3599  clel5  3605  reu7  3671  2reu5a  3683  0el  4274  n0snor2el  4724  uni0b  4826  iuncom  4888  iuncom4  4889  iuniin  4893  dfiunv2  4922  iunab  4938  iunn0  4952  iunin2  4956  iundif2  4959  iunun  4978  iunxiun  4982  iunpwss  4992  axrep6  5161  inuni  5210  reusv2lem5  5268  iunopab  5411  dffr2  5484  frc  5485  frminex  5499  dfepfr  5504  epfrc  5505  xpiundi  5586  xpiundir  5587  reliin  5654  iunxpf  5683  cnvuni  5721  dmiun  5746  dmopab2rex  5750  elres  5857  elidinxp  5878  dfima3  5899  dffr3  5929  rniun  5973  xpdifid  5992  dminxp  6004  imaco  6071  coiun  6076  dffr4  6132  tz6.26  6147  sucel  6232  isarep1  6412  rexrn  6830  ralrn  6831  elrnrexdmb  6833  fnasrn  6884  rexima  6977  ralima  6978  abrexco  6981  imaiun  6982  fliftcnv  7043  rexrnmpo  7269  iunpw  7473  abrexex2g  7647  el2xptp  7717  rdglem1  8034  tz7.49  8064  oarec  8171  omeu  8194  qsid  8346  eroveu  8375  ixp0  8478  fimax2g  8748  marypha2lem2  8884  dfsup2  8892  infcllem  8935  dfoi  8959  wemapsolem  8998  zfregcl  9042  zfreg  9043  zfregfr  9052  oemapso  9129  zfregs2  9159  infenaleph  9502  isinfcard  9503  kmlem7  9567  kmlem13  9573  fin23lem26  9736  dffin1-5  9799  fin12  9824  numth  9883  ac6n  9896  zorn2lem7  9913  zorng  9915  brdom7disj  9942  brdom6disj  9943  uniwun  10151  axgroth5  10235  axgroth4  10243  grothprim  10245  npomex  10407  genpass  10420  elreal  10542  dfinfre  11609  infrenegsup  11611  uzwo  12299  ublbneg  12321  xrinfmss2  12692  4fvwrd4  13022  fsuppmapnn0fiubex  13355  fsuppmapnn0ub  13358  mptnn0fsuppr  13362  hashge2el2dif  13834  dfrtrclrec2  14409  rexanuz  14697  rexfiuz  14699  clim0  14855  cbvsum  15044  incexc2  15185  cbvprod  15261  fprodle  15342  iprodmul  15349  divalglem10  15743  divalgb  15745  ncoprmlnprm  16058  pythagtriplem2  16144  pythagtriplem19  16160  pythagtrip  16161  pceu  16173  prmreclem6  16247  4sqlem12  16282  cshwshashlem1  16421  cshwshash  16430  imasaddfnlem  16793  isdrs2  17541  smndex1mgm  18064  smndex1n0mnd  18069  pmtrprfvalrn  18608  pgpfac1lem5  19194  dvdsrval  19391  opprunit  19407  lsmspsn  19849  lsmelval2  19850  islpidl  20012  mat1dimelbas  21076  mat1dimbas  21077  mdetunilem8  21224  pmatcollpw2lem  21382  tgval2  21561  ntreq0  21682  isclo2  21693  neiptopnei  21737  ist0-3  21950  tgcmp  22006  cmpfi  22013  is1stc2  22047  unisngl  22132  xkobval  22191  txtube  22245  txcmplem1  22246  xkococnlem  22264  eltsms  22738  metrest  23131  iscau3  23882  bcth  23933  pmltpc  24054  itg2i1fseq  24359  itg2cn  24367  plyun0  24794  aaliou3lem9  24946  1cubr  25428  dchrvmasumlema  26084  selbergsb  26159  ostth  26223  istrkg2ld  26254  tglowdim1i  26295  legtrid  26385  midex  26531  ishpg  26553  brbtwn2  26699  colinearalg  26704  ax5seg  26732  axpasch  26735  axlowdimlem6  26741  axeuclidlem  26756  axeuclid  26757  elntg2  26779  umgr2edg1  27001  umgr2edgneu  27004  nbgrsym  27153  isuvtx  27185  usgr2pth0  27554  wlkiswwlksupgr2  27663  clwwlknun  27897  4cycl2vnunb  28075  fusgreg2wsp  28121  lpni  28263  nmobndseqi  28562  hhcmpl  28983  shne0i  29231  nmcopexi  29810  nmcfnexi  29834  cdj3lem3b  30223  rexcom4f  30241  reuxfrdf  30262  iunin1f  30321  ofpreima  30428  intimafv  30470  fpwrelmapffslem  30494  tosglblem  30682  xrnarchi  30863  lsmsnorb  30999  ordtconnlem1  31277  lmdvg  31306  esumfsup  31439  reprsuc  31996  reprdifc  32008  bnj168  32110  bnj1185  32175  bnj1542  32239  bnj865  32305  bnj916  32315  bnj983  32333  bnj1176  32387  bnj1189  32391  bnj1296  32403  bnj1398  32416  bnj1450  32432  bnj1463  32437  nummin  32474  loop1cycl  32497  cvmliftlem15  32658  cvmlift2lem12  32674  satfvsuclem2  32720  satfvsucsuc  32725  satfdm  32729  satf0  32732  dmopab3rexdif  32765  dffr5  33102  imaindm  33135  dfon2lem9  33149  frpomin2  33192  soseq  33209  frrlem9  33244  noseponlem  33284  nosepon  33285  nolt02o  33312  brbigcup  33472  elfuns  33489  brimage  33500  brimg  33511  dfrecs2  33524  imagesset  33527  brub  33528  brsegle  33682  filnetlem4  33842  bj-rexcom4bv  34322  bj-rexcom4b  34323  bj-elsngl  34404  bj-rest10  34503  bj-restreg  34514  bj-mpomptALT  34534  nlpineqsn  34825  fvineqsneq  34829  iundif1  35031  matunitlindflem1  35053  poimirlem1  35058  poimirlem30  35087  poimirlem32  35089  poimir  35090  ismblfin  35098  volsupnfl  35102  itg2addnclem3  35110  fdc  35183  isfldidl  35506  eldmqsres2  35704  n0elqs  35743  rnxrncnvepres  35808  rnxrnidres  35809  dfcoels  35835  br1cossinres  35847  br1cossinidres  35849  br1cossincnvepres  35850  br1cossxrnidres  35851  br1cossxrncnvepres  35852  br1cossxrncnvssrres  35908  eldmqs1cossres  36053  prtlem10  36161  prter2  36177  islshpat  36313  lshpsmreu  36405  2dim  36766  islpln5  36831  lplnexatN  36859  islvol5  36875  dalem18  36977  dalem20  36989  lhpexle2  37306  lhpexle3  37308  lhpex2leN  37309  4atex2  37373  4atex2-0bOLDN  37375  cdlemftr3  37861  cdlemg17pq  37968  cdlemg19  37980  cdlemg21  37982  cdlemg33d  38005  dva1dim  38281  dih1dimatlem  38625  dihglb2  38638  dvh2dim  38741  mapdrvallem2  38941  mapdpglem3  38971  hdmapglem7a  39223  iunsn  39412  dffltz  39615  elrfirn  39636  isnacs2  39647  isnacs3  39651  sbc2rex  39728  4rexfrabdioph  39739  eldioph4b  39752  fphpd  39757  fiphp3d  39760  rencldnfilem  39761  rmxdioph  39957  expdiophlem1  39962  islnm2  40022  elimaint  40349  cnviun  40351  imaiun1  40352  coiun1  40353  elintima  40354  briunov2  40383  clsk3nimkb  40743  expandrexn  40999  prmunb2  41015  zfregs2VD  41547  evth2f  41644  evthf  41656  ndisj2  41685  fnlimabslt  42321  climbddf  42329  limsupub  42346  limsuppnflem  42352  limsupubuz  42355  limsupre2lem  42366  limsupreuz  42379  limsupvaluz2  42380  cnrefiisplem  42471  cnrefiisp  42472  stoweidlem28  42670  fourierdlem63  42811  fourierdlem65  42813  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem100  42848  sge0pnfmpt  43084  ovn0  43205  smfaddlem1  43396  smflimlem4  43407  2rexsb  43656  2rexrsb  43657  cbvrex2  43659  2reu8i  43669  copisnmnd  44429  pgrpgt2nabl  44768  islindeps  44862  lindslinindsimp1  44866  lindslinindsimp2  44872  islindeps2  44892  islininds2  44893  isldepslvec2  44894  ldepslinc  44918