Theorem rexbii 3251

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

Syntax hints:   ↔ wb 198   ∈ wcel 2166  ∃wrex 3118

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-rex 3123

This theorem is referenced by:  2rexbii  3252  rexnal2  3253  ralnex3  3256  r19.29r  3283  r19.29imd  3284  r19.41vv  3301  r19.42v  3302  r19.43  3303  rexcom13  3311  rexrot4  3313  3reeanv  3318  2ralor  3319  cbvrex2v  3392  rexcom4  3442  rexcom4a  3443  rexcom4b  3444  ceqsrex2v  3556  reu7  3626  0el  4168  n0snor2el  4580  uni0b  4685  iuncom  4747  iuncom4  4748  iuniin  4751  dfiunv2  4776  iunab  4786  iunn0  4800  iunin2  4804  iundif2  4807  iunun  4825  iunxiun  4829  iunpwss  4839  inuni  5048  reusv2lem5  5102  reuxfrd  5121  iunopab  5238  dffr2  5307  frc  5308  frminex  5322  dfepfr  5327  epfrc  5328  xpiundi  5406  xpiundir  5407  reliin  5475  iunxpf  5503  cnvuni  5541  dmiun  5565  elres  5671  elidinxp  5692  elridOLD  5695  dfima3  5710  dffr3  5739  rniun  5784  xpdifid  5803  dminxp  5815  imaco  5881  coiun  5886  dffr4  5936  tz6.26  5951  sucel  6036  isarep1  6210  rexrn  6610  ralrn  6611  elrnrexdmb  6613  fnasrn  6661  rexima  6753  ralima  6754  abrexco  6757  imaiun  6758  fliftcnv  6816  rexrnmpt2  7036  iunpw  7239  abrexex2g  7405  el2xptp  7473  rdglem1  7777  tz7.49  7806  oarec  7909  omeu  7932  qsid  8078  eroveu  8108  ixp0  8208  fimax2g  8475  marypha2lem2  8611  dfsup2  8619  infcllem  8662  dfoi  8685  wemapsolem  8724  zfregcl  8768  zfreg  8769  zfregfr  8778  oemapso  8856  zfregs2  8886  infenaleph  9227  isinfcard  9228  kmlem7  9293  kmlem13  9299  fin23lem26  9462  dffin1-5  9525  fin12  9550  numth  9609  ac6n  9622  zorn2lem7  9639  zorng  9641  brdom7disj  9668  brdom6disj  9669  uniwun  9877  axgroth5  9961  axgroth4  9969  grothprim  9971  npomex  10133  genpass  10146  elreal  10268  dfinfre  11334  infrenegsup  11336  uzwo  12034  ublbneg  12056  xrinfmss2  12429  4fvwrd4  12754  fsuppmapnn0fiubex  13086  fsuppmapnn0ub  13089  mptnn0fsuppr  13093  hashge2el2dif  13551  wrdlen1  13614  dfrtrclrec2  14174  rexanuz  14462  rexfiuz  14464  clim0  14614  cbvsum  14802  incexc2  14944  cbvprod  15018  fprodle  15099  iprodmul  15106  divalglem10  15499  divalgb  15501  ncoprmlnprm  15807  phisum  15866  pythagtriplem2  15893  pythagtriplem19  15909  pythagtrip  15910  pceu  15922  prmreclem6  15996  4sqlem12  16031  cshwshashlem1  16168  cshwshash  16177  imasaddfnlem  16541  isdrs2  17292  symgmov1  18162  pmtrprfvalrn  18258  pgpfac1lem5  18832  dvdsrval  18999  opprunit  19015  lsmspsn  19443  lsmelval2  19444  islpidl  19607  mat1dimelbas  20645  mat1dimbas  20646  mdetunilem8  20793  pmatcollpw2lem  20952  tgval2  21131  ntreq0  21252  isclo2  21263  neiptopnei  21307  ist0-3  21520  tgcmp  21575  cmpfi  21582  is1stc2  21616  unisngl  21701  xkobval  21760  txtube  21814  txcmplem1  21815  xkococnlem  21833  eltsms  22306  metrest  22699  iscau3  23446  bcth  23497  pmltpc  23616  itg2i1fseq  23921  itg2cn  23929  plyun0  24352  aaliou3lem9  24504  1cubr  24982  dchrvmasumlema  25602  selbergsb  25677  ostth  25741  istrkg2ld  25772  tglowdim1i  25813  tgdim01  25819  legtrid  25903  midex  26046  ishpg  26068  brbtwn2  26204  colinearalg  26209  ax5seg  26237  axpasch  26240  axlowdimlem6  26246  axeuclidlem  26261  axeuclid  26262  elntg2  26284  umgr2edg1  26507  umgr2edgneu  26510  nbgrsym  26660  isuvtx  26693  usgr2pth0  27067  wlkiswwlksupgr2  27176  clwwlknun  27487  4cycl2vnunb  27671  fusgreg2wsp  27717  lpni  27890  nmobndseqi  28189  hhcmpl  28612  shne0i  28862  nmcopexi  29441  nmcfnexi  29465  cdj3lem3b  29854  rexcom4f  29872  iunin1f  29922  ofpreima  30014  fpwrelmapffslem  30055  tosglblem  30214  xrnarchi  30283  ordtconnlem1  30515  lmdvg  30544  esumfsup  30677  reprsuc  31242  reprdifc  31254  bnj168  31345  bnj1185  31410  bnj1542  31473  bnj865  31539  bnj916  31549  bnj983  31567  bnj1176  31619  bnj1189  31623  bnj1296  31635  bnj1398  31648  bnj1450  31664  bnj1463  31669  cvmliftlem15  31826  cvmlift2lem12  31842  dffr5  32185  imaindm  32220  dfon2lem9  32234  frpomin2  32278  soseq  32293  noseponlem  32356  nosepon  32357  nolt02o  32384  brbigcup  32544  elfuns  32561  brimage  32572  brimg  32583  dfrecs2  32596  imagesset  32599  brub  32600  brsegle  32754  filnetlem4  32914  bj-rexcom4a  33390  bj-rexcom4bv  33391  bj-rexcom4b  33392  bj-elsngl  33478  bj-rest10  33564  bj-restreg  33575  bj-mpt2mptALT  33595  iundif1  33926  matunitlindflem1  33949  poimirlem1  33954  poimirlem30  33983  poimirlem32  33985  poimir  33986  ismblfin  33994  volsupnfl  33998  itg2addnclem3  34006  fdc  34083  isfldidl  34409  eldmqsres2  34603  n0elqs  34646  rnxrncnvepres  34706  rnxrnidres  34707  dfcoels  34733  br1cossinres  34745  br1cossinidres  34747  br1cossincnvepres  34748  br1cossxrnidres  34749  br1cossxrncnvepres  34750  br1cossxrncnvssrres  34806  prtlem10  34940  prter2  34956  islshpat  35092  lshpsmreu  35184  2dim  35545  islpln5  35610  lplnexatN  35638  islvol5  35654  dalem18  35756  dalem20  35768  lhpexle2  36085  lhpexle3  36087  lhpex2leN  36088  4atex2  36152  4atex2-0bOLDN  36154  cdlemftr3  36640  cdlemg17pq  36747  cdlemg19  36759  cdlemg21  36761  cdlemg33d  36784  dva1dim  37060  dih1dimatlem  37404  dihglb2  37417  dvh2dim  37520  mapdrvallem2  37720  mapdpglem3  37750  hdmapglem7a  38002  dffltz  38097  elrfirn  38102  isnacs2  38113  isnacs3  38117  sbc2rex  38195  4rexfrabdioph  38206  eldioph4b  38219  fphpd  38224  fiphp3d  38227  rencldnfilem  38228  rmxdioph  38426  expdiophlem1  38431  islnm2  38491  elimaint  38781  cnviun  38783  imaiun1  38784  coiun1  38785  elintima  38786  briunov2  38815  clsk3nimkb  39178  prmunb2  39350  zfregs2VD  39895  evth2f  39992  evthf  40004  ndisj2  40035  fnlimabslt  40706  climbddf  40714  limsupub  40731  limsuppnflem  40737  limsupubuz  40740  limsupre2lem  40751  limsupreuz  40764  limsupvaluz2  40765  cnrefiisplem  40850  cnrefiisp  40851  stoweidlem28  41039  fourierdlem63  41180  fourierdlem65  41182  fourierdlem89  41206  fourierdlem90  41207  fourierdlem91  41208  fourierdlem100  41217  sge0pnfmpt  41453  ovn0  41574  smfaddlem1  41765  smflimlem4  41776  2rexsb  41996  2rexrsb  41997  cbvrex2  41999  2reu5a  42002  copisnmnd  42656  pgrpgt2nabl  42994  islindeps  43089  lindslinindsimp1  43093  lindslinindsimp2  43099  islindeps2  43119  islininds2  43120  isldepslvec2  43121  ldepslinc  43145