Theorem eleq1d 2262

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  eleq12d  2264  eqeltrd  2270  eqneltrd  2289  eqneltrrd  2290  rspcimdv  2865  rspcimedv  2866  reuind  2965  sbcel2g  3101  sbccsb2g  3110  breq1  4032  breq2  4033  inex1g  4165  intexr  4179  pwexg  4209  prexg  4240  opelopabsb  4290  pofun  4343  seex  4366  uniex  4468  uniexg  4470  unexb  4473  abnexg  4477  reusv3  4491  rabxfrd  4500  onun2  4522  onsucelsucexmid  4562  ordsucunielexmid  4563  dcextest  4613  tfisi  4619  peano2  4627  seinxp  4730  opabid2  4793  opeliunxp2  4802  elrn2g  4852  opeldm  4865  opeldmg  4867  elreldm  4888  elrn2  4904  opelresg  4949  elsnres  4979  iss  4988  elimasng  5033  issref  5048  rnxpid  5100  unielrel  5193  dffun5r  5266  funopg  5288  brprcneu  5547  tz6.12f  5583  fvelrnb  5604  ssimaex  5618  dmfco  5625  fvmpt3  5636  mptfvex  5643  fvmptf  5650  respreima  5686  fvelrn  5689  ffnfvf  5717  ffvresb  5721  fmptco  5724  fmptcof  5725  fsn  5730  fressnfv  5745  fnex  5780  funfvima  5790  funfvima3  5792  f1mpt  5814  fliftfuns  5841  isoselem  5863  ovrspc2v  5944  ffnov  6022  fovcld  6023  ovmpos  6042  ov2gf  6043  ovg  6057  funimassov  6068  caovclg  6071  elovmpo  6117  off  6143  caofdig  6159  fnexALT  6163  focdmex  6167  f1stres  6212  f2ndres  6213  xp1st  6218  xp2nd  6219  elxp6  6222  oprssdmm  6224  unielxp  6227  fmpox  6253  mpofvex  6256  opeliunxp2f  6291  dftpos4  6316  smoel  6353  tfrlem3-2d  6365  tfrlem8  6371  tfrlem9  6372  tfrlemibxssdm  6380  tfrlemi1  6385  tfrexlem  6387  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  rdgtfr  6427  rdgon  6439  frecabex  6451  frecabcl  6452  frecfcllem  6457  frecsuclem  6459  nnacl  6533  nnmcl  6534  nnmordi  6569  nnaordex  6581  nnm00  6583  erexb  6612  qliftfuns  6673  ixpsnval  6755  elixp2  6756  resixp  6787  mptelixpg  6788  elixpsn  6789  fundmen  6860  fopwdom  6892  xpf1o  6900  dif1en  6935  diffitest  6943  diffifi  6950  inffiexmid  6962  unfiexmid  6974  unfidisj  6978  fiintim  6985  xpfi  6986  ssfirab  6990  fnfi  6995  iunfidisj  7005  snexxph  7009  fidcenumlemr  7014  elfi2  7031  ctssdccl  7170  isnumi  7242  cc2lem  7326  cc3  7328  addnidpig  7396  indpi  7402  dfplpq2  7414  addclnq  7435  mulclnq  7436  nnnq0lem1  7506  addclnq0  7511  mulclnq0  7512  nqpnq0nq  7513  distrnq0  7519  prloc  7551  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  genpml  7577  genpmu  7578  addnqprl  7589  addnqpru  7590  mulnqprl  7628  mulnqpru  7629  ltexprlemell  7658  ltexprlemelu  7659  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  ltexpri  7673  recexprlemm  7684  recexprlemdisj  7690  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  recexpr  7698  addclsr  7813  mulclsr  7814  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  suplocsr  7869  pitonn  7908  peano2nnnn  7913  axaddrcl  7925  axmulrcl  7927  peano5nnnn  7952  axpre-suploclemres  7961  negreb  8284  negf1o  8401  eqord1  8502  eqord2  8503  cju  8980  peano2nn  8994  nn1m1nn  9000  nnaddcl  9002  nnmulcl  9003  nnsub  9021  nndivtr  9024  un0addcl  9273  un0mulcl  9274  elnnnn0  9283  elz  9319  nnnegz  9320  znegclb  9350  zaddcllempos  9354  zaddcllemneg  9356  zaddcl  9357  nzadd  9369  zmulcl  9370  elz2  9388  zneo  9418  nneoor  9419  zeo  9422  peano5uzti  9425  zindd  9435  uzp1  9626  uzaddcl  9651  supinfneg  9660  infsupneg  9661  supminfex  9662  ublbneg  9678  eqreznegel  9679  negm  9680  qmulz  9688  qnegcl  9701  irradd  9711  irrmul  9712  fzrev2  10151  negqmod0  10402  frec2uzuzd  10473  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgsuctlem  10494  xnn0nnen  10508  iseqovex  10529  seq3val  10531  seqvalcd  10532  seq3-1  10533  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3clss  10542  monoord  10556  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seqf1og  10592  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  seq3distr  10603  ser3ge0  10607  expp1  10617  expcllem  10621  expcl2lemap  10622  m1expcl2  10632  facnn  10798  fac0  10799  fac1  10800  faccl  10806  facdiv  10809  facndiv  10810  bccmpl  10825  bcn2  10835  bccl  10838  fihasheqf1oi  10858  seq3coll  10913  shftlem  10960  shftf  10974  seq3shft  10982  cjval  10989  cjth  10990  remim  11004  uzin2  11131  caubnd2  11261  negfi  11371  xrmaxltsup  11401  clim  11424  clim2  11426  climshftlemg  11445  climcn1  11451  climcn2  11452  iserex  11482  climub  11487  climserle  11488  climcau  11490  serf0  11495  sumfct  11517  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsumgcl  11529  fsum3  11530  fsumf1o  11533  isumss  11534  isumss2  11536  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumsplitf  11551  sumpr  11556  sumtp  11557  fsumm1  11559  fsum1p  11561  isummulc2  11569  fsum2dlemstep  11577  fisumcom2  11581  fsumshftm  11588  fisum0diag2  11590  fsummulc2  11591  fsumge1  11604  fsum00  11605  fsumabs  11608  telfsumo  11609  telfsumo2  11610  fsumparts  11613  fsumrelem  11614  fsumiun  11620  binomlem  11626  isumshft  11633  isum1p  11635  isumrpcl  11637  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  mertenslem2  11679  mertensabs  11680  clim2prod  11682  prodfap0  11688  prodfrecap  11689  prodfdivap  11690  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  prodfct  11730  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodmul  11734  fprodm1  11741  fprod1p  11742  fprodm1s  11744  fprodp1s  11745  fprodcl2lem  11748  fprodabs  11759  fprod2dlemstep  11765  fprodcnv  11768  fprodcom2fi  11769  fprodrec  11772  fproddivapf  11774  fprodsplitf  11775  fprodsplit1f  11777  fprodle  11783  zeo3  12009  mulsucdiv2z  12026  zob  12032  nn0o1gt2  12046  nno  12047  nn0o  12048  infssuzex  12086  infssuzcldc  12088  zsupssdc  12091  uzwodc  12174  qnumdencl  12325  pcqcl  12444  pcxnn0cl  12448  pcxcl  12449  pcgcd1  12466  dvdsprmpweqle  12475  pcmpt  12481  pcmpt2  12482  pcmptdvds  12483  infpnlem2  12498  1arith  12505  elgz  12509  mul4sq  12532  4sqlem13m  12541  4sqlem17  12545  4sqlem18  12546  4sqlem19  12547  znnen  12555  ennnfonelemj0  12558  ennnfonelemg  12560  ennnfonelemom  12565  ctinfom  12585  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunctlemfo  12596  ssnnctlemct  12603  infpn2  12613  isstruct2im  12628  isstruct2r  12629  imasaddfnlemg  12897  ercpbl  12914  xpsfrnel2  12929  mgmsscl  12944  mgm1  12953  sgrppropd  12996  mndpropd  13021  issubm  13044  0subm  13056  insubm  13057  mhmima  13063  mulgsubcl  13206  issubg  13243  subgex  13246  issubg2m  13259  issubg4m  13263  0subg  13269  isnsg  13272  isnsg2  13273  nsgbi  13274  isnsg3  13277  elnmz  13278  nmzbi  13279  nmzsubg  13280  nmznsg  13283  releqgg  13290  eqgex  13291  eqgval  13293  eqgid  13296  ghmrn  13327  ghmnsgima  13338  eqgabl  13400  ablnsg  13404  gsumfzmhm2  13414  isrng  13430  issrg  13461  srgfcl  13469  isring  13496  iscrng  13499  dvdsrd  13590  unitsubm  13615  isrim0  13657  issubrng  13695  subrngringnsg  13701  issubrng2  13706  opprsubrngg  13707  issubrg  13717  subrgsubm  13730  subrgugrp  13736  issubrg2  13737  issubrg3  13743  subrgpropd  13749  aprval  13778  aprsym  13780  islmod  13787  lmodlema  13788  islmodd  13789  lmodprop2d  13844  rmodislmodlem  13846  rmodislmod  13847  lsssetm  13852  islssmd  13855  lssclg  13860  lsslss  13877  lsspropdg  13927  islidlm  13975  rnglidlmcl  13976  isridlrng  13978  rnglidlmmgm  13992  isridl  14000  gsumfzfsumlemm  14075  psrbag  14155  uniopn  14169  inopn  14171  fiinopn  14172  iscld  14271  iuncld  14283  tgrest  14337  iscn  14365  cnpval  14366  iscnp  14367  tgcn  14376  ssidcn  14378  lmbrf  14383  cnpnei  14387  cnima  14388  cnconst2  14401  cnrest2  14404  cnptopresti  14406  cnptoprest  14407  lmres  14416  lmtopcnp  14418  txbasval  14435  tx1cn  14437  tx2cn  14438  txcnp  14439  txcnmpt  14441  txdis1cn  14446  txlm  14447  cnmpt11  14451  cnmpt12  14455  cnmpt21  14459  cnmpt22  14462  ishmeo  14472  hmeoopn  14479  hmeocld  14480  qtopbasss  14689  fsumcncntop  14724  expcncf  14763  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthdec  14798  limccl  14813  ellimc3apf  14814  cnmptlimc  14828  limccoap  14832  2irrexpq  15108  2irrexpqap  15110  lgsval  15120  lgsval2lem  15126  lgsdir2lem4  15147  lgsdir2  15149  m1lgs  15192  mul2sq  15203  2sqlem6  15207  bdinex1g  15393  bj-intexr  15400  bj-prexg  15403  bj-uniex  15409  bj-uniexg  15410  bdunexb  15412  bj-indsuc  15420  exmidsbthrlem  15512  qdencn  15517  iswomni0  15541