Theorem eleq1d 2298

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 2292	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12d  2300  eqeltrd  2306  eqneltrd  2325  eqneltrrd  2326  rspcimdv  2908  rspcimedv  2909  reuind  3008  sbcel2g  3145  sbccsb2g  3154  breq1  4086  breq2  4087  inex1g  4220  intexr  4234  pwexg  4264  prexg  4295  opelopabsb  4348  pofun  4403  seex  4426  uniex  4528  uniexg  4530  unexb  4533  abnexg  4537  reusv3  4551  rabxfrd  4560  onun2  4582  onsucelsucexmid  4622  ordsucunielexmid  4623  dcextest  4673  tfisi  4679  peano2  4687  seinxp  4790  opabid2  4853  opeliunxp2  4862  elrn2g  4912  opeldm  4926  opeldmg  4928  elreldm  4950  elrn2  4966  opelresg  5012  elsnres  5042  iss  5051  elimasng  5096  issref  5111  rnxpid  5163  unielrel  5256  dffun5r  5330  funopg  5352  brprcneu  5622  tz6.12f  5658  fvelrnb  5683  ssimaex  5697  dmfco  5704  fvmpt3  5715  mptfvex  5722  fvmptf  5729  respreima  5765  fvelrn  5768  ffnfvf  5796  ffvresb  5800  fmptco  5803  fmptcof  5804  fsn  5809  fressnfv  5830  fnex  5865  funfvima  5875  funfvima3  5877  f1mpt  5901  fliftfuns  5928  isoselem  5950  ovrspc2v  6033  ffnov  6114  fovcld  6115  ovmpos  6134  ov2gf  6135  ovg  6150  funimassov  6161  caovclg  6164  elovmpo  6210  off  6237  caofdig  6258  fnexALT  6262  focdmex  6266  f1stres  6311  f2ndres  6312  xp1st  6317  xp2nd  6318  elxp6  6321  oprssdmm  6323  unielxp  6326  fmpox  6352  mpofvex  6357  opeliunxp2f  6390  dftpos4  6415  smoel  6452  tfrlem3-2d  6464  tfrlem8  6470  tfrlem9  6471  tfrlemibxssdm  6479  tfrlemi1  6484  tfrexlem  6486  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgtfr  6526  rdgon  6538  frecabex  6550  frecabcl  6551  frecfcllem  6556  frecsuclem  6558  nnacl  6634  nnmcl  6635  nnmordi  6670  nnaordex  6682  nnm00  6684  erexb  6713  qliftfuns  6774  ixpsnval  6856  elixp2  6857  resixp  6888  mptelixpg  6889  elixpsn  6890  fundmen  6967  fopwdom  7005  xpf1o  7013  dif1en  7049  diffitest  7057  diffifi  7064  inffiexmid  7079  unfiexmid  7091  unfidisj  7095  prfidceq  7101  fiintim  7104  xpfi  7105  ssfirab  7109  fnfi  7114  iunfidisj  7124  snexxph  7128  fidcenumlemr  7133  elfi2  7150  ctssdccl  7289  isnumi  7365  cc2lem  7463  cc3  7465  addnidpig  7534  indpi  7540  dfplpq2  7552  addclnq  7573  mulclnq  7574  nnnq0lem1  7644  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  distrnq0  7657  prloc  7689  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  genpml  7715  genpmu  7716  addnqprl  7727  addnqpru  7728  mulnqprl  7766  mulnqpru  7767  ltexprlemell  7796  ltexprlemelu  7797  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  ltexpri  7811  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  addclsr  7951  mulclsr  7952  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  suplocsr  8007  pitonn  8046  peano2nnnn  8051  axaddrcl  8063  axmulrcl  8065  peano5nnnn  8090  axpre-suploclemres  8099  negreb  8422  negf1o  8539  eqord1  8641  eqord2  8642  cju  9119  peano2nn  9133  nn1m1nn  9139  nnaddcl  9141  nnmulcl  9142  nnsub  9160  nndivtr  9163  un0addcl  9413  un0mulcl  9414  elnnnn0  9423  elz  9459  nnnegz  9460  znegclb  9490  zaddcllempos  9494  zaddcllemneg  9496  zaddcl  9497  nzadd  9510  zmulcl  9511  elz2  9529  zneo  9559  nneoor  9560  zeo  9563  peano5uzti  9566  zindd  9576  uzp1  9768  uzaddcl  9793  supinfneg  9802  infsupneg  9803  supminfex  9804  ublbneg  9820  eqreznegel  9821  negm  9822  qmulz  9830  qnegcl  9843  irradd  9853  irrmul  9854  fzrev2  10293  infssuzex  10465  infssuzcldc  10467  zsupssdc  10470  negqmod0  10565  frec2uzuzd  10636  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  xnn0nnen  10671  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1og  10755  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  seq3distr  10766  ser3ge0  10770  expp1  10780  expcllem  10784  expcl2lemap  10785  m1expcl2  10795  facnn  10961  fac0  10962  fac1  10963  faccl  10969  facdiv  10972  facndiv  10973  bccmpl  10988  bcn2  10998  bccl  11001  fihasheqf1oi  11021  seq3coll  11077  ccatalpha  11161  reuccatpfxs1lem  11293  reuccatpfxs1  11294  shftlem  11342  shftf  11356  seq3shft  11364  cjval  11371  cjth  11372  remim  11386  uzin2  11513  caubnd2  11643  negfi  11754  xrmaxltsup  11784  clim  11807  clim2  11809  climshftlemg  11828  climcn1  11834  climcn2  11835  iserex  11865  climub  11870  climserle  11871  climcau  11873  serf0  11878  sumfct  11900  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  fsumf1o  11916  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumsplitf  11934  sumpr  11939  sumtp  11940  fsumm1  11942  fsum1p  11944  isummulc2  11952  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fisum0diag2  11973  fsummulc2  11974  fsumge1  11987  fsum00  11988  fsumabs  11991  telfsumo  11992  telfsumo2  11993  fsumparts  11996  fsumrelem  11997  fsumiun  12003  binomlem  12009  isumshft  12016  isum1p  12018  isumrpcl  12020  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  mertenslem2  12062  mertensabs  12063  clim2prod  12065  prodfap0  12071  prodfrecap  12072  prodfdivap  12073  prodrbdclem  12097  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  prodfct  12113  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodmul  12117  fprodm1  12124  fprod1p  12125  fprodm1s  12127  fprodp1s  12128  fprodcl2lem  12131  fprodabs  12142  fprod2dlemstep  12148  fprodcnv  12151  fprodcom2fi  12152  fprodrec  12155  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  fprodle  12166  zeo3  12394  mulsucdiv2z  12411  zob  12417  nn0o1gt2  12431  nno  12432  nn0o  12433  uzwodc  12573  qnumdencl  12724  pcqcl  12844  pcxnn0cl  12848  pcxcl  12849  pcgcd1  12866  dvdsprmpweqle  12875  pcmpt  12881  pcmpt2  12882  pcmptdvds  12883  infpnlem2  12898  1arith  12905  elgz  12909  mul4sq  12932  4sqlem13m  12941  4sqlem17  12945  4sqlem18  12946  4sqlem19  12947  znnen  12984  ennnfonelemj0  12987  ennnfonelemg  12989  ennnfonelemom  12994  ctinfom  13014  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  ctiunctlemudc  13023  ctiunctlemfo  13025  ssnnctlemct  13032  infpn2  13042  isstruct2im  13057  isstruct2r  13058  imasaddfnlemg  13362  ercpbl  13379  xpsfrnel2  13394  mgmsscl  13409  mgm1  13418  sgrppropd  13461  mndpropd  13488  issubm  13520  0subm  13532  insubm  13533  mhmima  13539  mulgsubcl  13688  issubg  13725  subgex  13728  issubg2m  13741  issubg4m  13745  0subg  13751  isnsg  13754  isnsg2  13755  nsgbi  13756  isnsg3  13759  elnmz  13760  nmzbi  13761  nmzsubg  13762  nmznsg  13765  releqgg  13772  eqgex  13773  eqgval  13775  eqgid  13778  ghmrn  13809  ghmnsgima  13820  eqgabl  13882  ablnsg  13886  gsumfzmhm2  13896  isrng  13912  issrg  13943  srgfcl  13951  isring  13978  iscrng  13981  dvdsrd  14073  unitsubm  14098  isrim0  14140  issubrng  14178  subrngringnsg  14184  issubrng2  14189  opprsubrngg  14190  issubrg  14200  subrgsubm  14213  subrgugrp  14219  issubrg2  14220  issubrg3  14226  subrgpropd  14232  aprval  14261  aprsym  14263  islmod  14270  lmodlema  14271  islmodd  14272  lmodprop2d  14327  rmodislmodlem  14329  rmodislmod  14330  lsssetm  14335  islssmd  14338  lssclg  14343  lsslss  14360  lsspropdg  14410  islidlm  14458  rnglidlmcl  14459  isridlrng  14461  rnglidlmmgm  14475  isridl  14483  gsumfzfsumlemm  14566  psrbag  14648  psr1clfi  14667  uniopn  14690  inopn  14692  fiinopn  14693  iscld  14792  iuncld  14804  tgrest  14858  iscn  14886  cnpval  14887  iscnp  14888  tgcn  14897  ssidcn  14899  lmbrf  14904  cnpnei  14908  cnima  14909  cnconst2  14922  cnrest2  14925  cnptopresti  14927  cnptoprest  14928  lmres  14937  lmtopcnp  14939  txbasval  14956  tx1cn  14958  tx2cn  14959  txcnp  14960  txcnmpt  14962  txdis1cn  14967  txlm  14968  cnmpt11  14972  cnmpt12  14976  cnmpt21  14980  cnmpt22  14983  ishmeo  14993  hmeoopn  15000  hmeocld  15001  qtopbasss  15210  fsumcncntop  15256  expcn  15258  expcncf  15298  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  ivthinc  15332  ivthdec  15333  limccl  15348  ellimc3apf  15349  cnmptlimc  15363  limccoap  15367  dvmptfsum  15414  plycolemc  15447  plycj  15450  2irrexpq  15665  2irrexpqap  15667  fsumdvdsmul  15680  perfect  15690  lgsval  15698  lgsval2lem  15704  lgsdir2lem4  15725  lgsdir2  15727  m1lgs  15779  2lgs  15798  mul2sq  15810  2sqlem6  15814  wlkcprim  16091  isclwwlk  16132  clwwlk1loop  16136  clwwlkccatlem  16137  bdinex1g  16319  bj-intexr  16326  bj-prexg  16329  bj-uniex  16335  bj-uniexg  16336  bdunexb  16338  bj-indsuc  16346  exmidsbthrlem  16450  qdencn  16455  iswomni0  16479