Theorem eleq1d 2275

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq1d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq1 2269	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12d  2277  eqeltrd  2283  eqneltrd  2302  eqneltrrd  2303  rspcimdv  2882  rspcimedv  2883  reuind  2982  sbcel2g  3118  sbccsb2g  3127  breq1  4053  breq2  4054  inex1g  4187  intexr  4201  pwexg  4231  prexg  4262  opelopabsb  4313  pofun  4366  seex  4389  uniex  4491  uniexg  4493  unexb  4496  abnexg  4500  reusv3  4514  rabxfrd  4523  onun2  4545  onsucelsucexmid  4585  ordsucunielexmid  4586  dcextest  4636  tfisi  4642  peano2  4650  seinxp  4753  opabid2  4816  opeliunxp2  4825  elrn2g  4875  opeldm  4889  opeldmg  4891  elreldm  4912  elrn2  4928  opelresg  4974  elsnres  5004  iss  5013  elimasng  5058  issref  5073  rnxpid  5125  unielrel  5218  dffun5r  5291  funopg  5313  brprcneu  5581  tz6.12f  5617  fvelrnb  5638  ssimaex  5652  dmfco  5659  fvmpt3  5670  mptfvex  5677  fvmptf  5684  respreima  5720  fvelrn  5723  ffnfvf  5751  ffvresb  5755  fmptco  5758  fmptcof  5759  fsn  5764  fressnfv  5783  fnex  5818  funfvima  5828  funfvima3  5830  f1mpt  5852  fliftfuns  5879  isoselem  5901  ovrspc2v  5982  ffnov  6061  fovcld  6062  ovmpos  6081  ov2gf  6082  ovg  6097  funimassov  6108  caovclg  6111  elovmpo  6157  off  6183  caofdig  6204  fnexALT  6208  focdmex  6212  f1stres  6257  f2ndres  6258  xp1st  6263  xp2nd  6264  elxp6  6267  oprssdmm  6269  unielxp  6272  fmpox  6298  mpofvex  6303  opeliunxp2f  6336  dftpos4  6361  smoel  6398  tfrlem3-2d  6410  tfrlem8  6416  tfrlem9  6417  tfrlemibxssdm  6425  tfrlemi1  6430  tfrexlem  6432  tfr1onlemsucfn  6438  tfr1onlemsucaccv  6439  tfr1onlembxssdm  6441  tfr1onlembfn  6442  tfr1onlemaccex  6446  tfr1onlemres  6447  tfri1dALT  6449  tfrcllemsucfn  6451  tfrcllemsucaccv  6452  tfrcllembxssdm  6454  tfrcllembfn  6455  tfrcllemaccex  6459  tfrcllemres  6460  tfrcl  6462  rdgtfr  6472  rdgon  6484  frecabex  6496  frecabcl  6497  frecfcllem  6502  frecsuclem  6504  nnacl  6578  nnmcl  6579  nnmordi  6614  nnaordex  6626  nnm00  6628  erexb  6657  qliftfuns  6718  ixpsnval  6800  elixp2  6801  resixp  6832  mptelixpg  6833  elixpsn  6834  fundmen  6911  fopwdom  6947  xpf1o  6955  dif1en  6990  diffitest  6998  diffifi  7005  inffiexmid  7017  unfiexmid  7029  unfidisj  7033  prfidceq  7039  fiintim  7042  xpfi  7043  ssfirab  7047  fnfi  7052  iunfidisj  7062  snexxph  7066  fidcenumlemr  7071  elfi2  7088  ctssdccl  7227  isnumi  7303  cc2lem  7393  cc3  7395  addnidpig  7464  indpi  7470  dfplpq2  7482  addclnq  7503  mulclnq  7504  nnnq0lem1  7574  addclnq0  7579  mulclnq0  7580  nqpnq0nq  7581  distrnq0  7587  prloc  7619  prarloclemlo  7622  prarloclem3  7625  prarloclem5  7628  genpml  7645  genpmu  7646  addnqprl  7657  addnqpru  7658  mulnqprl  7696  mulnqpru  7697  ltexprlemell  7726  ltexprlemelu  7727  ltexprlemdisj  7734  ltexprlemloc  7735  ltexprlemrl  7738  ltexprlemru  7740  ltexpri  7741  recexprlemm  7752  recexprlemdisj  7758  recexprlemloc  7759  recexprlem1ssl  7761  recexprlem1ssu  7762  recexpr  7766  addclsr  7881  mulclsr  7882  suplocsrlemb  7934  suplocsrlempr  7935  suplocsrlem  7936  suplocsr  7937  pitonn  7976  peano2nnnn  7981  axaddrcl  7993  axmulrcl  7995  peano5nnnn  8020  axpre-suploclemres  8029  negreb  8352  negf1o  8469  eqord1  8571  eqord2  8572  cju  9049  peano2nn  9063  nn1m1nn  9069  nnaddcl  9071  nnmulcl  9072  nnsub  9090  nndivtr  9093  un0addcl  9343  un0mulcl  9344  elnnnn0  9353  elz  9389  nnnegz  9390  znegclb  9420  zaddcllempos  9424  zaddcllemneg  9426  zaddcl  9427  nzadd  9440  zmulcl  9441  elz2  9459  zneo  9489  nneoor  9490  zeo  9493  peano5uzti  9496  zindd  9506  uzp1  9697  uzaddcl  9722  supinfneg  9731  infsupneg  9732  supminfex  9733  ublbneg  9749  eqreznegel  9750  negm  9751  qmulz  9759  qnegcl  9772  irradd  9782  irrmul  9783  fzrev2  10222  infssuzex  10393  infssuzcldc  10395  zsupssdc  10398  negqmod0  10493  frec2uzuzd  10564  frecuzrdgrrn  10570  frec2uzrdg  10571  frecuzrdgrcl  10572  frecuzrdgsuc  10576  frecuzrdgrclt  10577  frecuzrdgg  10578  frecuzrdgsuctlem  10585  xnn0nnen  10599  iseqovex  10620  seq3val  10622  seqvalcd  10623  seq3-1  10624  seqf  10626  seq3p1  10627  seqovcd  10629  seqp1cd  10632  seq3clss  10633  monoord  10647  monoord2  10648  ser3mono  10649  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seq3caopr2  10655  seqcaopr2g  10656  iseqf1olemjpcl  10670  iseqf1olemqpcl  10671  iseqf1olemfvp  10672  seq3f1olemqsumkj  10673  seq3f1olemqsum  10675  seq3f1oleml  10678  seq3f1o  10679  seqf1og  10683  seq3homo  10689  seq3z  10690  seqhomog  10692  seqfeq4g  10693  seq3distr  10694  ser3ge0  10698  expp1  10708  expcllem  10712  expcl2lemap  10713  m1expcl2  10723  facnn  10889  fac0  10890  fac1  10891  faccl  10897  facdiv  10900  facndiv  10901  bccmpl  10916  bcn2  10926  bccl  10929  fihasheqf1oi  10949  seq3coll  11004  shftlem  11197  shftf  11211  seq3shft  11219  cjval  11226  cjth  11227  remim  11241  uzin2  11368  caubnd2  11498  negfi  11609  xrmaxltsup  11639  clim  11662  clim2  11664  climshftlemg  11683  climcn1  11689  climcn2  11690  iserex  11720  climub  11725  climserle  11726  climcau  11728  serf0  11733  sumfct  11755  sumrbdclem  11758  fsum3cvg  11759  summodclem3  11761  summodclem2a  11762  zsumdc  11765  fsumgcl  11767  fsum3  11768  fsumf1o  11771  isumss  11772  isumss2  11774  fsum3cvg2  11775  fsum3ser  11778  fsumcl2lem  11779  fsumsplitf  11789  sumpr  11794  sumtp  11795  fsumm1  11797  fsum1p  11799  isummulc2  11807  fsum2dlemstep  11815  fisumcom2  11819  fsumshftm  11826  fisum0diag2  11828  fsummulc2  11829  fsumge1  11842  fsum00  11843  fsumabs  11846  telfsumo  11847  telfsumo2  11848  fsumparts  11851  fsumrelem  11852  fsumiun  11858  binomlem  11864  isumshft  11871  isum1p  11873  isumrpcl  11875  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  cvgratnnlemseq  11907  cvgratnnlemabsle  11908  cvgratnnlemfm  11910  cvgratnnlemrate  11911  cvgratnn  11912  cvgratz  11913  mertenslem2  11917  mertensabs  11918  clim2prod  11920  prodfap0  11926  prodfrecap  11927  prodfdivap  11928  prodrbdclem  11952  fproddccvg  11953  prodmodclem3  11956  prodmodclem2a  11957  zproddc  11960  fprodseq  11964  prodfct  11968  fprodf1o  11969  prodssdc  11970  fprodssdc  11971  fprodmul  11972  fprodm1  11979  fprod1p  11980  fprodm1s  11982  fprodp1s  11983  fprodcl2lem  11986  fprodabs  11997  fprod2dlemstep  12003  fprodcnv  12006  fprodcom2fi  12007  fprodrec  12010  fproddivapf  12012  fprodsplitf  12013  fprodsplit1f  12015  fprodle  12021  zeo3  12249  mulsucdiv2z  12266  zob  12272  nn0o1gt2  12286  nno  12287  nn0o  12288  uzwodc  12428  qnumdencl  12579  pcqcl  12699  pcxnn0cl  12703  pcxcl  12704  pcgcd1  12721  dvdsprmpweqle  12730  pcmpt  12736  pcmpt2  12737  pcmptdvds  12738  infpnlem2  12753  1arith  12760  elgz  12764  mul4sq  12787  4sqlem13m  12796  4sqlem17  12800  4sqlem18  12801  4sqlem19  12802  znnen  12839  ennnfonelemj0  12842  ennnfonelemg  12844  ennnfonelemom  12849  ctinfom  12869  ctiunctlemu1st  12875  ctiunctlemu2nd  12876  ctiunctlemudc  12878  ctiunctlemfo  12880  ssnnctlemct  12887  infpn2  12897  isstruct2im  12912  isstruct2r  12913  imasaddfnlemg  13216  ercpbl  13233  xpsfrnel2  13248  mgmsscl  13263  mgm1  13272  sgrppropd  13315  mndpropd  13342  issubm  13374  0subm  13386  insubm  13387  mhmima  13393  mulgsubcl  13542  issubg  13579  subgex  13582  issubg2m  13595  issubg4m  13599  0subg  13605  isnsg  13608  isnsg2  13609  nsgbi  13610  isnsg3  13613  elnmz  13614  nmzbi  13615  nmzsubg  13616  nmznsg  13619  releqgg  13626  eqgex  13627  eqgval  13629  eqgid  13632  ghmrn  13663  ghmnsgima  13674  eqgabl  13736  ablnsg  13740  gsumfzmhm2  13750  isrng  13766  issrg  13797  srgfcl  13805  isring  13832  iscrng  13835  dvdsrd  13926  unitsubm  13951  isrim0  13993  issubrng  14031  subrngringnsg  14037  issubrng2  14042  opprsubrngg  14043  issubrg  14053  subrgsubm  14066  subrgugrp  14072  issubrg2  14073  issubrg3  14079  subrgpropd  14085  aprval  14114  aprsym  14116  islmod  14123  lmodlema  14124  islmodd  14125  lmodprop2d  14180  rmodislmodlem  14182  rmodislmod  14183  lsssetm  14188  islssmd  14191  lssclg  14196  lsslss  14213  lsspropdg  14263  islidlm  14311  rnglidlmcl  14312  isridlrng  14314  rnglidlmmgm  14328  isridl  14336  gsumfzfsumlemm  14419  psrbag  14501  psr1clfi  14520  uniopn  14543  inopn  14545  fiinopn  14546  iscld  14645  iuncld  14657  tgrest  14711  iscn  14739  cnpval  14740  iscnp  14741  tgcn  14750  ssidcn  14752  lmbrf  14757  cnpnei  14761  cnima  14762  cnconst2  14775  cnrest2  14778  cnptopresti  14780  cnptoprest  14781  lmres  14790  lmtopcnp  14792  txbasval  14809  tx1cn  14811  tx2cn  14812  txcnp  14813  txcnmpt  14815  txdis1cn  14820  txlm  14821  cnmpt11  14825  cnmpt12  14829  cnmpt21  14833  cnmpt22  14836  ishmeo  14846  hmeoopn  14853  hmeocld  14854  qtopbasss  15063  fsumcncntop  15109  expcn  15111  expcncf  15151  ivthinclemlopn  15178  ivthinclemlr  15179  ivthinclemuopn  15180  ivthinclemur  15181  ivthinclemdisj  15182  ivthinclemloc  15183  ivthinc  15185  ivthdec  15186  limccl  15201  ellimc3apf  15202  cnmptlimc  15216  limccoap  15220  dvmptfsum  15267  plycolemc  15300  plycj  15303  2irrexpq  15518  2irrexpqap  15520  fsumdvdsmul  15533  perfect  15543  lgsval  15551  lgsval2lem  15557  lgsdir2lem4  15578  lgsdir2  15580  m1lgs  15632  2lgs  15651  mul2sq  15663  2sqlem6  15667  bdinex1g  15971  bj-intexr  15978  bj-prexg  15981  bj-uniex  15987  bj-uniexg  15988  bdunexb  15990  bj-indsuc  15998  exmidsbthrlem  16096  qdencn  16101  iswomni0  16125