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  2866  rspcimedv  2867  reuind  2966  sbcel2g  3102  sbccsb2g  3111  breq1  4033  breq2  4034  inex1g  4166  intexr  4180  pwexg  4210  prexg  4241  opelopabsb  4291  pofun  4344  seex  4367  uniex  4469  uniexg  4471  unexb  4474  abnexg  4478  reusv3  4492  rabxfrd  4501  onun2  4523  onsucelsucexmid  4563  ordsucunielexmid  4564  dcextest  4614  tfisi  4620  peano2  4628  seinxp  4731  opabid2  4794  opeliunxp2  4803  elrn2g  4853  opeldm  4866  opeldmg  4868  elreldm  4889  elrn2  4905  opelresg  4950  elsnres  4980  iss  4989  elimasng  5034  issref  5049  rnxpid  5101  unielrel  5194  dffun5r  5267  funopg  5289  brprcneu  5548  tz6.12f  5584  fvelrnb  5605  ssimaex  5619  dmfco  5626  fvmpt3  5637  mptfvex  5644  fvmptf  5651  respreima  5687  fvelrn  5690  ffnfvf  5718  ffvresb  5722  fmptco  5725  fmptcof  5726  fsn  5731  fressnfv  5746  fnex  5781  funfvima  5791  funfvima3  5793  f1mpt  5815  fliftfuns  5842  isoselem  5864  ovrspc2v  5945  ffnov  6023  fovcld  6024  ovmpos  6043  ov2gf  6044  ovg  6059  funimassov  6070  caovclg  6073  elovmpo  6119  off  6145  caofdig  6161  fnexALT  6165  focdmex  6169  f1stres  6214  f2ndres  6215  xp1st  6220  xp2nd  6221  elxp6  6224  oprssdmm  6226  unielxp  6229  fmpox  6255  mpofvex  6260  opeliunxp2f  6293  dftpos4  6318  smoel  6355  tfrlem3-2d  6367  tfrlem8  6373  tfrlem9  6374  tfrlemibxssdm  6382  tfrlemi1  6387  tfrexlem  6389  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  tfri1dALT  6406  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  rdgtfr  6429  rdgon  6441  frecabex  6453  frecabcl  6454  frecfcllem  6459  frecsuclem  6461  nnacl  6535  nnmcl  6536  nnmordi  6571  nnaordex  6583  nnm00  6585  erexb  6614  qliftfuns  6675  ixpsnval  6757  elixp2  6758  resixp  6789  mptelixpg  6790  elixpsn  6791  fundmen  6862  fopwdom  6894  xpf1o  6902  dif1en  6937  diffitest  6945  diffifi  6952  inffiexmid  6964  unfiexmid  6976  unfidisj  6980  fiintim  6987  xpfi  6988  ssfirab  6992  fnfi  6997  iunfidisj  7007  snexxph  7011  fidcenumlemr  7016  elfi2  7033  ctssdccl  7172  isnumi  7244  cc2lem  7328  cc3  7330  addnidpig  7398  indpi  7404  dfplpq2  7416  addclnq  7437  mulclnq  7438  nnnq0lem1  7508  addclnq0  7513  mulclnq0  7514  nqpnq0nq  7515  distrnq0  7521  prloc  7553  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  genpml  7579  genpmu  7580  addnqprl  7591  addnqpru  7592  mulnqprl  7630  mulnqpru  7631  ltexprlemell  7660  ltexprlemelu  7661  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  ltexpri  7675  recexprlemm  7686  recexprlemdisj  7692  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  recexpr  7700  addclsr  7815  mulclsr  7816  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  suplocsr  7871  pitonn  7910  peano2nnnn  7915  axaddrcl  7927  axmulrcl  7929  peano5nnnn  7954  axpre-suploclemres  7963  negreb  8286  negf1o  8403  eqord1  8504  eqord2  8505  cju  8982  peano2nn  8996  nn1m1nn  9002  nnaddcl  9004  nnmulcl  9005  nnsub  9023  nndivtr  9026  un0addcl  9276  un0mulcl  9277  elnnnn0  9286  elz  9322  nnnegz  9323  znegclb  9353  zaddcllempos  9357  zaddcllemneg  9359  zaddcl  9360  nzadd  9372  zmulcl  9373  elz2  9391  zneo  9421  nneoor  9422  zeo  9425  peano5uzti  9428  zindd  9438  uzp1  9629  uzaddcl  9654  supinfneg  9663  infsupneg  9664  supminfex  9665  ublbneg  9681  eqreznegel  9682  negm  9683  qmulz  9691  qnegcl  9704  irradd  9714  irrmul  9715  fzrev2  10154  negqmod0  10405  frec2uzuzd  10476  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  xnn0nnen  10511  iseqovex  10532  seq3val  10534  seqvalcd  10535  seq3-1  10536  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3clss  10545  monoord  10559  monoord2  10560  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seqf1og  10595  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  seq3distr  10606  ser3ge0  10610  expp1  10620  expcllem  10624  expcl2lemap  10625  m1expcl2  10635  facnn  10801  fac0  10802  fac1  10803  faccl  10809  facdiv  10812  facndiv  10813  bccmpl  10828  bcn2  10838  bccl  10841  fihasheqf1oi  10861  seq3coll  10916  shftlem  10963  shftf  10977  seq3shft  10985  cjval  10992  cjth  10993  remim  11007  uzin2  11134  caubnd2  11264  negfi  11374  xrmaxltsup  11404  clim  11427  clim2  11429  climshftlemg  11448  climcn1  11454  climcn2  11455  iserex  11485  climub  11490  climserle  11491  climcau  11493  serf0  11498  sumfct  11520  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsumgcl  11532  fsum3  11533  fsumf1o  11536  isumss  11537  isumss2  11539  fsum3cvg2  11540  fsum3ser  11543  fsumcl2lem  11544  fsumsplitf  11554  sumpr  11559  sumtp  11560  fsumm1  11562  fsum1p  11564  isummulc2  11572  fsum2dlemstep  11580  fisumcom2  11584  fsumshftm  11591  fisum0diag2  11593  fsummulc2  11594  fsumge1  11607  fsum00  11608  fsumabs  11611  telfsumo  11612  telfsumo2  11613  fsumparts  11616  fsumrelem  11617  fsumiun  11623  binomlem  11629  isumshft  11636  isum1p  11638  isumrpcl  11640  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslem2  11682  mertensabs  11683  clim2prod  11685  prodfap0  11691  prodfrecap  11692  prodfdivap  11693  prodrbdclem  11717  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  prodfct  11733  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  fprodm1  11744  fprod1p  11745  fprodm1s  11747  fprodp1s  11748  fprodcl2lem  11751  fprodabs  11762  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  fprodrec  11775  fproddivapf  11777  fprodsplitf  11778  fprodsplit1f  11780  fprodle  11786  zeo3  12012  mulsucdiv2z  12029  zob  12035  nn0o1gt2  12049  nno  12050  nn0o  12051  infssuzex  12089  infssuzcldc  12091  zsupssdc  12094  uzwodc  12177  qnumdencl  12328  pcqcl  12447  pcxnn0cl  12451  pcxcl  12452  pcgcd1  12469  dvdsprmpweqle  12478  pcmpt  12484  pcmpt2  12485  pcmptdvds  12486  infpnlem2  12501  1arith  12508  elgz  12512  mul4sq  12535  4sqlem13m  12544  4sqlem17  12548  4sqlem18  12549  4sqlem19  12550  znnen  12558  ennnfonelemj0  12561  ennnfonelemg  12563  ennnfonelemom  12568  ctinfom  12588  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunctlemfo  12599  ssnnctlemct  12606  infpn2  12616  isstruct2im  12631  isstruct2r  12632  imasaddfnlemg  12900  ercpbl  12917  xpsfrnel2  12932  mgmsscl  12947  mgm1  12956  sgrppropd  12999  mndpropd  13024  issubm  13047  0subm  13059  insubm  13060  mhmima  13066  mulgsubcl  13209  issubg  13246  subgex  13249  issubg2m  13262  issubg4m  13266  0subg  13272  isnsg  13275  isnsg2  13276  nsgbi  13277  isnsg3  13280  elnmz  13281  nmzbi  13282  nmzsubg  13283  nmznsg  13286  releqgg  13293  eqgex  13294  eqgval  13296  eqgid  13299  ghmrn  13330  ghmnsgima  13341  eqgabl  13403  ablnsg  13407  gsumfzmhm2  13417  isrng  13433  issrg  13464  srgfcl  13472  isring  13499  iscrng  13502  dvdsrd  13593  unitsubm  13618  isrim0  13660  issubrng  13698  subrngringnsg  13704  issubrng2  13709  opprsubrngg  13710  issubrg  13720  subrgsubm  13733  subrgugrp  13739  issubrg2  13740  issubrg3  13746  subrgpropd  13752  aprval  13781  aprsym  13783  islmod  13790  lmodlema  13791  islmodd  13792  lmodprop2d  13847  rmodislmodlem  13849  rmodislmod  13850  lsssetm  13855  islssmd  13858  lssclg  13863  lsslss  13880  lsspropdg  13930  islidlm  13978  rnglidlmcl  13979  isridlrng  13981  rnglidlmmgm  13995  isridl  14003  gsumfzfsumlemm  14086  psrbag  14166  uniopn  14180  inopn  14182  fiinopn  14183  iscld  14282  iuncld  14294  tgrest  14348  iscn  14376  cnpval  14377  iscnp  14378  tgcn  14387  ssidcn  14389  lmbrf  14394  cnpnei  14398  cnima  14399  cnconst2  14412  cnrest2  14415  cnptopresti  14417  cnptoprest  14418  lmres  14427  lmtopcnp  14429  txbasval  14446  tx1cn  14448  tx2cn  14449  txcnp  14450  txcnmpt  14452  txdis1cn  14457  txlm  14458  cnmpt11  14462  cnmpt12  14466  cnmpt21  14470  cnmpt22  14473  ishmeo  14483  hmeoopn  14490  hmeocld  14491  qtopbasss  14700  fsumcncntop  14746  expcn  14748  expcncf  14788  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthdec  14823  limccl  14838  ellimc3apf  14839  cnmptlimc  14853  limccoap  14857  dvmptfsum  14904  plycolemc  14936  plycj  14939  2irrexpq  15149  2irrexpqap  15151  lgsval  15161  lgsval2lem  15167  lgsdir2lem4  15188  lgsdir2  15190  m1lgs  15242  2lgs  15261  mul2sq  15273  2sqlem6  15277  bdinex1g  15463  bj-intexr  15470  bj-prexg  15473  bj-uniex  15479  bj-uniexg  15480  bdunexb  15482  bj-indsuc  15490  exmidsbthrlem  15582  qdencn  15587  iswomni0  15611