Theorem eleq1d 2300

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eqeltrd  2308  eqneltrd  2327  eqneltrrd  2328  rspcimdv  2912  rspcimedv  2913  reuind  3012  sbcel2g  3149  sbccsb2g  3158  breq1  4096  breq2  4097  inex1g  4230  intexr  4245  pwexg  4276  prexg  4307  opelopabsb  4360  pofun  4415  seex  4438  uniex  4540  uniexg  4542  unexb  4545  abnexg  4549  reusv3  4563  rabxfrd  4572  onun2  4594  onsucelsucexmid  4634  ordsucunielexmid  4635  dcextest  4685  tfisi  4691  peano2  4699  seinxp  4803  opabid2  4867  opeliunxp2  4876  elrn2g  4926  opeldm  4940  opeldmg  4942  elreldm  4964  elrn2  4980  opelresg  5026  elsnres  5056  iss  5065  xpexcnvm  5098  elimasng  5111  issref  5126  rnxpid  5178  unielrel  5271  dffun5r  5345  funopg  5367  brprcneu  5641  tz6.12f  5677  fvelrnb  5702  ssimaex  5716  dmfco  5723  fvmpt3  5734  mptfvex  5741  fvmptf  5748  respreima  5783  fvelrn  5786  ffnfvf  5814  ffvresb  5818  fmptco  5821  fmptcof  5822  fsn  5827  fsn2g  5830  fressnfv  5849  fnex  5884  funfvima  5896  funfvima3  5898  f1mpt  5922  fliftfuns  5949  isoselem  5971  ovrspc2v  6054  ffnov  6135  fovcld  6136  ovmpos  6155  ov2gf  6156  ovg  6171  funimassov  6182  caovclg  6185  elovmpo  6231  off  6257  caofdig  6278  fnexALT  6282  focdmex  6286  f1stres  6331  f2ndres  6332  xp1st  6337  xp2nd  6338  elxp6  6341  oprssdmm  6343  unielxp  6346  fmpox  6374  mpofvex  6379  elmpom  6412  suppofss1dcl  6442  suppofss2dcl  6443  opeliunxp2f  6447  dftpos4  6472  smoel  6509  tfrlem3-2d  6521  tfrlem8  6527  tfrlem9  6528  tfrlemibxssdm  6536  tfrlemi1  6541  tfrexlem  6543  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgtfr  6583  rdgon  6595  frecabex  6607  frecabcl  6608  frecfcllem  6613  frecsuclem  6615  nnacl  6691  nnmcl  6692  nnmordi  6727  nnaordex  6739  nnm00  6741  erexb  6770  qliftfuns  6831  ixpsnval  6913  elixp2  6914  resixp  6945  mptelixpg  6946  elixpsn  6947  fundmen  7024  fopwdom  7065  xpf1o  7073  dif1en  7111  diffitest  7119  diffifi  7126  inffiexmid  7141  unfiexmid  7153  unfidisj  7157  prfidceq  7163  fiintim  7166  xpfi  7167  ssfirab  7172  fnfi  7178  iunfidisj  7188  snexxph  7192  fidcenumlemr  7197  elfi2  7214  ctssdccl  7353  isnumi  7429  cc2lem  7528  cc3  7530  addnidpig  7599  indpi  7605  dfplpq2  7617  addclnq  7638  mulclnq  7639  nnnq0lem1  7709  addclnq0  7714  mulclnq0  7715  nqpnq0nq  7716  distrnq0  7722  prloc  7754  prarloclemlo  7757  prarloclem3  7760  prarloclem5  7763  genpml  7780  genpmu  7781  addnqprl  7792  addnqpru  7793  mulnqprl  7831  mulnqpru  7832  ltexprlemell  7861  ltexprlemelu  7862  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  ltexpri  7876  recexprlemm  7887  recexprlemdisj  7893  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  recexpr  7901  addclsr  8016  mulclsr  8017  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  suplocsr  8072  pitonn  8111  peano2nnnn  8116  axaddrcl  8128  axmulrcl  8130  peano5nnnn  8155  axpre-suploclemres  8164  negreb  8487  negf1o  8604  eqord1  8706  eqord2  8707  cju  9184  peano2nn  9198  nn1m1nn  9204  nnaddcl  9206  nnmulcl  9207  nnsub  9225  nndivtr  9228  un0addcl  9478  un0mulcl  9479  elnnnn0  9488  elz  9526  nnnegz  9527  znegclb  9557  zaddcllempos  9561  zaddcllemneg  9563  zaddcl  9564  nzadd  9577  zmulcl  9578  elz2  9596  zneo  9626  nneoor  9627  zeo  9630  peano5uzti  9633  zindd  9643  uzp1  9835  uzaddcl  9865  supinfneg  9874  infsupneg  9875  supminfex  9876  ublbneg  9892  eqreznegel  9893  negm  9894  qmulz  9902  qnegcl  9915  irradd  9925  irrmul  9926  fzrev2  10365  infssuzex  10539  infssuzcldc  10541  zsupssdc  10544  negqmod0  10639  frec2uzuzd  10710  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  frecuzrdgsuctlem  10731  xnn0nnen  10745  iseqovex  10766  seq3val  10768  seqvalcd  10769  seq3-1  10770  seqf  10772  seq3p1  10773  seqovcd  10775  seqp1cd  10778  seq3clss  10779  monoord  10793  monoord2  10794  ser3mono  10795  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seq3caopr2  10801  seqcaopr2g  10802  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsum  10821  seq3f1oleml  10824  seq3f1o  10825  seqf1og  10829  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  seq3distr  10840  ser3ge0  10844  expp1  10854  expcllem  10858  expcl2lemap  10859  m1expcl2  10869  facnn  11035  fac0  11036  fac1  11037  faccl  11043  facdiv  11046  facndiv  11047  bccmpl  11062  bcn2  11072  bccl  11075  fihasheqf1oi  11095  seq3coll  11152  ccatalpha  11239  reuccatpfxs1lem  11376  reuccatpfxs1  11377  shftlem  11439  shftf  11453  seq3shft  11461  cjval  11468  cjth  11469  remim  11483  uzin2  11610  caubnd2  11740  negfi  11851  xrmaxltsup  11881  clim  11904  clim2  11906  climshftlemg  11925  climcn1  11931  climcn2  11932  iserex  11962  climub  11967  climserle  11968  climcau  11970  serf0  11975  sumfct  11997  sumrbdclem  12001  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  fsumf1o  12014  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumsplitf  12032  sumpr  12037  sumtp  12038  fsumm1  12040  fsum1p  12042  isummulc2  12050  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fisum0diag2  12071  fsummulc2  12072  fsumge1  12085  fsum00  12086  fsumabs  12089  telfsumo  12090  telfsumo2  12091  fsumparts  12094  fsumrelem  12095  fsumiun  12101  binomlem  12107  isumshft  12114  isum1p  12116  isumrpcl  12118  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  cvgratz  12156  mertenslem2  12160  mertensabs  12161  clim2prod  12163  prodfap0  12169  prodfrecap  12170  prodfdivap  12171  prodrbdclem  12195  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  prodfct  12211  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodmul  12215  fprodm1  12222  fprod1p  12223  fprodm1s  12225  fprodp1s  12226  fprodcl2lem  12229  fprodabs  12240  fprod2dlemstep  12246  fprodcnv  12249  fprodcom2fi  12250  fprodrec  12253  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  fprodle  12264  zeo3  12492  mulsucdiv2z  12509  zob  12515  nn0o1gt2  12529  nno  12530  nn0o  12531  uzwodc  12671  qnumdencl  12822  pcqcl  12942  pcxnn0cl  12946  pcxcl  12947  pcgcd1  12964  dvdsprmpweqle  12973  pcmpt  12979  pcmpt2  12980  pcmptdvds  12981  infpnlem2  12996  1arith  13003  elgz  13007  mul4sq  13030  4sqlem13m  13039  4sqlem17  13043  4sqlem18  13044  4sqlem19  13045  znnen  13082  ennnfonelemj0  13085  ennnfonelemg  13087  ennnfonelemom  13092  ctinfom  13112  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunctlemfo  13123  ssnnctlemct  13130  infpn2  13140  isstruct2im  13155  isstruct2r  13156  imasaddfnlemg  13460  ercpbl  13477  xpsfrnel2  13492  mgmsscl  13507  mgm1  13516  sgrppropd  13559  mndpropd  13586  issubm  13618  0subm  13630  insubm  13631  mhmima  13637  mulgsubcl  13786  issubg  13823  subgex  13826  issubg2m  13839  issubg4m  13843  0subg  13849  isnsg  13852  isnsg2  13853  nsgbi  13854  isnsg3  13857  elnmz  13858  nmzbi  13859  nmzsubg  13860  nmznsg  13863  releqgg  13870  eqgex  13871  eqgval  13873  eqgid  13876  ghmrn  13907  ghmnsgima  13918  eqgabl  13980  ablnsg  13984  gsumfzmhm2  13994  isrng  14011  issrg  14042  srgfcl  14050  isring  14077  iscrng  14080  dvdsrd  14172  unitsubm  14197  isrim0  14239  issubrng  14277  subrngringnsg  14283  issubrng2  14288  opprsubrngg  14289  issubrg  14299  subrgsubm  14312  subrgugrp  14318  issubrg2  14319  issubrg3  14325  subrgpropd  14331  aprval  14361  aprsym  14363  islmod  14370  lmodlema  14371  islmodd  14372  lmodprop2d  14427  rmodislmodlem  14429  rmodislmod  14430  lsssetm  14435  islssmd  14438  lssclg  14443  lsslss  14460  lsspropdg  14510  islidlm  14558  rnglidlmcl  14559  isridlrng  14561  rnglidlmmgm  14575  isridl  14583  gsumfzfsumlemm  14666  psrbag  14748  psr1clfi  14772  uniopn  14795  inopn  14797  fiinopn  14798  iscld  14897  iuncld  14909  tgrest  14963  iscn  14991  cnpval  14992  iscnp  14993  tgcn  15002  ssidcn  15004  lmbrf  15009  cnpnei  15013  cnima  15014  cnconst2  15027  cnrest2  15030  cnptopresti  15032  cnptoprest  15033  lmres  15042  lmtopcnp  15044  txbasval  15061  tx1cn  15063  tx2cn  15064  txcnp  15065  txcnmpt  15067  txdis1cn  15072  txlm  15073  cnmpt11  15077  cnmpt12  15081  cnmpt21  15085  cnmpt22  15088  ishmeo  15098  hmeoopn  15105  hmeocld  15106  qtopbasss  15315  fsumcncntop  15361  expcn  15363  expcncf  15403  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  ivthinc  15437  ivthdec  15438  limccl  15453  ellimc3apf  15454  cnmptlimc  15468  limccoap  15472  dvmptfsum  15519  plycolemc  15552  plycj  15555  2irrexpq  15770  2irrexpqap  15772  pellexlem1  15774  fsumdvdsmul  15788  perfect  15798  lgsval  15806  lgsval2lem  15812  lgsdir2lem4  15833  lgsdir2  15835  m1lgs  15887  2lgs  15906  mul2sq  15918  2sqlem6  15922  wlkcprim  16274  isclwwlk  16318  clwwlk1loop  16323  clwwlkccatlem  16324  clwwlkn1  16342  loopclwwlkn1b  16343  clwwlkn1loopb  16344  clwwlkn2  16345  clwwlkext2edg  16346  umgr2cwwk2dif  16348  s2elclwwlknon2  16360  clwwlknonex2lem2  16362  clwwlknonex2  16363  eupth2lem2dc  16383  eulerpathprum  16404  bdinex1g  16600  bj-intexr  16607  bj-prexg  16610  bj-uniex  16616  bj-uniexg  16617  bdunexb  16619  bj-indsuc  16627  exmidsbthrlem  16733  qdencn  16738  repiecef  16743  iswomni0  16767  gfsumval  16792  gfsumcl  16799