Theorem eleq1d 2265

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12d  2267  eqeltrd  2273  eqneltrd  2292  eqneltrrd  2293  rspcimdv  2869  rspcimedv  2870  reuind  2969  sbcel2g  3105  sbccsb2g  3114  breq1  4036  breq2  4037  inex1g  4169  intexr  4183  pwexg  4213  prexg  4244  opelopabsb  4294  pofun  4347  seex  4370  uniex  4472  uniexg  4474  unexb  4477  abnexg  4481  reusv3  4495  rabxfrd  4504  onun2  4526  onsucelsucexmid  4566  ordsucunielexmid  4567  dcextest  4617  tfisi  4623  peano2  4631  seinxp  4734  opabid2  4797  opeliunxp2  4806  elrn2g  4856  opeldm  4869  opeldmg  4871  elreldm  4892  elrn2  4908  opelresg  4953  elsnres  4983  iss  4992  elimasng  5037  issref  5052  rnxpid  5104  unielrel  5197  dffun5r  5270  funopg  5292  brprcneu  5551  tz6.12f  5587  fvelrnb  5608  ssimaex  5622  dmfco  5629  fvmpt3  5640  mptfvex  5647  fvmptf  5654  respreima  5690  fvelrn  5693  ffnfvf  5721  ffvresb  5725  fmptco  5728  fmptcof  5729  fsn  5734  fressnfv  5749  fnex  5784  funfvima  5794  funfvima3  5796  f1mpt  5818  fliftfuns  5845  isoselem  5867  ovrspc2v  5948  ffnov  6026  fovcld  6027  ovmpos  6046  ov2gf  6047  ovg  6062  funimassov  6073  caovclg  6076  elovmpo  6122  off  6148  caofdig  6164  fnexALT  6168  focdmex  6172  f1stres  6217  f2ndres  6218  xp1st  6223  xp2nd  6224  elxp6  6227  oprssdmm  6229  unielxp  6232  fmpox  6258  mpofvex  6263  opeliunxp2f  6296  dftpos4  6321  smoel  6358  tfrlem3-2d  6370  tfrlem8  6376  tfrlem9  6377  tfrlemibxssdm  6385  tfrlemi1  6390  tfrexlem  6392  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfr1onlemres  6407  tfri1dALT  6409  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  rdgtfr  6432  rdgon  6444  frecabex  6456  frecabcl  6457  frecfcllem  6462  frecsuclem  6464  nnacl  6538  nnmcl  6539  nnmordi  6574  nnaordex  6586  nnm00  6588  erexb  6617  qliftfuns  6678  ixpsnval  6760  elixp2  6761  resixp  6792  mptelixpg  6793  elixpsn  6794  fundmen  6865  fopwdom  6897  xpf1o  6905  dif1en  6940  diffitest  6948  diffifi  6955  inffiexmid  6967  unfiexmid  6979  unfidisj  6983  prfidceq  6989  fiintim  6992  xpfi  6993  ssfirab  6997  fnfi  7002  iunfidisj  7012  snexxph  7016  fidcenumlemr  7021  elfi2  7038  ctssdccl  7177  isnumi  7249  cc2lem  7333  cc3  7335  addnidpig  7403  indpi  7409  dfplpq2  7421  addclnq  7442  mulclnq  7443  nnnq0lem1  7513  addclnq0  7518  mulclnq0  7519  nqpnq0nq  7520  distrnq0  7526  prloc  7558  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  genpml  7584  genpmu  7585  addnqprl  7596  addnqpru  7597  mulnqprl  7635  mulnqpru  7636  ltexprlemell  7665  ltexprlemelu  7666  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  ltexpri  7680  recexprlemm  7691  recexprlemdisj  7697  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  recexpr  7705  addclsr  7820  mulclsr  7821  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  suplocsr  7876  pitonn  7915  peano2nnnn  7920  axaddrcl  7932  axmulrcl  7934  peano5nnnn  7959  axpre-suploclemres  7968  negreb  8291  negf1o  8408  eqord1  8510  eqord2  8511  cju  8988  peano2nn  9002  nn1m1nn  9008  nnaddcl  9010  nnmulcl  9011  nnsub  9029  nndivtr  9032  un0addcl  9282  un0mulcl  9283  elnnnn0  9292  elz  9328  nnnegz  9329  znegclb  9359  zaddcllempos  9363  zaddcllemneg  9365  zaddcl  9366  nzadd  9378  zmulcl  9379  elz2  9397  zneo  9427  nneoor  9428  zeo  9431  peano5uzti  9434  zindd  9444  uzp1  9635  uzaddcl  9660  supinfneg  9669  infsupneg  9670  supminfex  9671  ublbneg  9687  eqreznegel  9688  negm  9689  qmulz  9697  qnegcl  9710  irradd  9720  irrmul  9721  fzrev2  10160  infssuzex  10323  infssuzcldc  10325  zsupssdc  10328  negqmod0  10423  frec2uzuzd  10494  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgsuctlem  10515  xnn0nnen  10529  iseqovex  10550  seq3val  10552  seqvalcd  10553  seq3-1  10554  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3clss  10563  monoord  10577  monoord2  10578  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seqf1og  10613  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  seq3distr  10624  ser3ge0  10628  expp1  10638  expcllem  10642  expcl2lemap  10643  m1expcl2  10653  facnn  10819  fac0  10820  fac1  10821  faccl  10827  facdiv  10830  facndiv  10831  bccmpl  10846  bcn2  10856  bccl  10859  fihasheqf1oi  10879  seq3coll  10934  shftlem  10981  shftf  10995  seq3shft  11003  cjval  11010  cjth  11011  remim  11025  uzin2  11152  caubnd2  11282  negfi  11393  xrmaxltsup  11423  clim  11446  clim2  11448  climshftlemg  11467  climcn1  11473  climcn2  11474  iserex  11504  climub  11509  climserle  11510  climcau  11512  serf0  11517  sumfct  11539  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  fsumf1o  11555  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsum3ser  11562  fsumcl2lem  11563  fsumsplitf  11573  sumpr  11578  sumtp  11579  fsumm1  11581  fsum1p  11583  isummulc2  11591  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fisum0diag2  11612  fsummulc2  11613  fsumge1  11626  fsum00  11627  fsumabs  11630  telfsumo  11631  telfsumo2  11632  fsumparts  11635  fsumrelem  11636  fsumiun  11642  binomlem  11648  isumshft  11655  isum1p  11657  isumrpcl  11659  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  mertenslem2  11701  mertensabs  11702  clim2prod  11704  prodfap0  11710  prodfrecap  11711  prodfdivap  11712  prodrbdclem  11736  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  prodfct  11752  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  fprodm1  11763  fprod1p  11764  fprodm1s  11766  fprodp1s  11767  fprodcl2lem  11770  fprodabs  11781  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  fprodrec  11794  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  fprodle  11805  zeo3  12033  mulsucdiv2z  12050  zob  12056  nn0o1gt2  12070  nno  12071  nn0o  12072  uzwodc  12204  qnumdencl  12355  pcqcl  12475  pcxnn0cl  12479  pcxcl  12480  pcgcd1  12497  dvdsprmpweqle  12506  pcmpt  12512  pcmpt2  12513  pcmptdvds  12514  infpnlem2  12529  1arith  12536  elgz  12540  mul4sq  12563  4sqlem13m  12572  4sqlem17  12576  4sqlem18  12577  4sqlem19  12578  znnen  12615  ennnfonelemj0  12618  ennnfonelemg  12620  ennnfonelemom  12625  ctinfom  12645  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunctlemfo  12656  ssnnctlemct  12663  infpn2  12673  isstruct2im  12688  isstruct2r  12689  imasaddfnlemg  12957  ercpbl  12974  xpsfrnel2  12989  mgmsscl  13004  mgm1  13013  sgrppropd  13056  mndpropd  13081  issubm  13104  0subm  13116  insubm  13117  mhmima  13123  mulgsubcl  13266  issubg  13303  subgex  13306  issubg2m  13319  issubg4m  13323  0subg  13329  isnsg  13332  isnsg2  13333  nsgbi  13334  isnsg3  13337  elnmz  13338  nmzbi  13339  nmzsubg  13340  nmznsg  13343  releqgg  13350  eqgex  13351  eqgval  13353  eqgid  13356  ghmrn  13387  ghmnsgima  13398  eqgabl  13460  ablnsg  13464  gsumfzmhm2  13474  isrng  13490  issrg  13521  srgfcl  13529  isring  13556  iscrng  13559  dvdsrd  13650  unitsubm  13675  isrim0  13717  issubrng  13755  subrngringnsg  13761  issubrng2  13766  opprsubrngg  13767  issubrg  13777  subrgsubm  13790  subrgugrp  13796  issubrg2  13797  issubrg3  13803  subrgpropd  13809  aprval  13838  aprsym  13840  islmod  13847  lmodlema  13848  islmodd  13849  lmodprop2d  13904  rmodislmodlem  13906  rmodislmod  13907  lsssetm  13912  islssmd  13915  lssclg  13920  lsslss  13937  lsspropdg  13987  islidlm  14035  rnglidlmcl  14036  isridlrng  14038  rnglidlmmgm  14052  isridl  14060  gsumfzfsumlemm  14143  psrbag  14223  uniopn  14237  inopn  14239  fiinopn  14240  iscld  14339  iuncld  14351  tgrest  14405  iscn  14433  cnpval  14434  iscnp  14435  tgcn  14444  ssidcn  14446  lmbrf  14451  cnpnei  14455  cnima  14456  cnconst2  14469  cnrest2  14472  cnptopresti  14474  cnptoprest  14475  lmres  14484  lmtopcnp  14486  txbasval  14503  tx1cn  14505  tx2cn  14506  txcnp  14507  txcnmpt  14509  txdis1cn  14514  txlm  14515  cnmpt11  14519  cnmpt12  14523  cnmpt21  14527  cnmpt22  14530  ishmeo  14540  hmeoopn  14547  hmeocld  14548  qtopbasss  14757  fsumcncntop  14803  expcn  14805  expcncf  14845  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthdec  14880  limccl  14895  ellimc3apf  14896  cnmptlimc  14910  limccoap  14914  dvmptfsum  14961  plycolemc  14994  plycj  14997  2irrexpq  15212  2irrexpqap  15214  fsumdvdsmul  15227  perfect  15237  lgsval  15245  lgsval2lem  15251  lgsdir2lem4  15272  lgsdir2  15274  m1lgs  15326  2lgs  15345  mul2sq  15357  2sqlem6  15361  bdinex1g  15547  bj-intexr  15554  bj-prexg  15557  bj-uniex  15563  bj-uniexg  15564  bdunexb  15566  bj-indsuc  15574  exmidsbthrlem  15666  qdencn  15671  iswomni0  15695