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  2909  rspcimedv  2910  reuind  3009  sbcel2g  3146  sbccsb2g  3155  breq1  4089  breq2  4090  inex1g  4223  intexr  4238  pwexg  4268  prexg  4299  opelopabsb  4352  pofun  4407  seex  4430  uniex  4532  uniexg  4534  unexb  4537  abnexg  4541  reusv3  4555  rabxfrd  4564  onun2  4586  onsucelsucexmid  4626  ordsucunielexmid  4627  dcextest  4677  tfisi  4683  peano2  4691  seinxp  4795  opabid2  4859  opeliunxp2  4868  elrn2g  4918  opeldm  4932  opeldmg  4934  elreldm  4956  elrn2  4972  opelresg  5018  elsnres  5048  iss  5057  elimasng  5102  issref  5117  rnxpid  5169  unielrel  5262  dffun5r  5336  funopg  5358  brprcneu  5628  tz6.12f  5664  fvelrnb  5689  ssimaex  5703  dmfco  5710  fvmpt3  5721  mptfvex  5728  fvmptf  5735  respreima  5771  fvelrn  5774  ffnfvf  5802  ffvresb  5806  fmptco  5809  fmptcof  5810  fsn  5815  fressnfv  5836  fnex  5871  funfvima  5881  funfvima3  5883  f1mpt  5907  fliftfuns  5934  isoselem  5956  ovrspc2v  6039  ffnov  6120  fovcld  6121  ovmpos  6140  ov2gf  6141  ovg  6156  funimassov  6167  caovclg  6170  elovmpo  6216  off  6243  caofdig  6264  fnexALT  6268  focdmex  6272  f1stres  6317  f2ndres  6318  xp1st  6323  xp2nd  6324  elxp6  6327  oprssdmm  6329  unielxp  6332  fmpox  6360  mpofvex  6365  elmpom  6398  opeliunxp2f  6399  dftpos4  6424  smoel  6461  tfrlem3-2d  6473  tfrlem8  6479  tfrlem9  6480  tfrlemibxssdm  6488  tfrlemi1  6493  tfrexlem  6495  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  rdgtfr  6535  rdgon  6547  frecabex  6559  frecabcl  6560  frecfcllem  6565  frecsuclem  6567  nnacl  6643  nnmcl  6644  nnmordi  6679  nnaordex  6691  nnm00  6693  erexb  6722  qliftfuns  6783  ixpsnval  6865  elixp2  6866  resixp  6897  mptelixpg  6898  elixpsn  6899  fundmen  6976  fopwdom  7017  xpf1o  7025  dif1en  7061  diffitest  7069  diffifi  7076  inffiexmid  7091  unfiexmid  7103  unfidisj  7107  prfidceq  7113  fiintim  7116  xpfi  7117  ssfirab  7121  fnfi  7126  iunfidisj  7136  snexxph  7140  fidcenumlemr  7145  elfi2  7162  ctssdccl  7301  isnumi  7377  cc2lem  7475  cc3  7477  addnidpig  7546  indpi  7552  dfplpq2  7564  addclnq  7585  mulclnq  7586  nnnq0lem1  7656  addclnq0  7661  mulclnq0  7662  nqpnq0nq  7663  distrnq0  7669  prloc  7701  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  genpml  7727  genpmu  7728  addnqprl  7739  addnqpru  7740  mulnqprl  7778  mulnqpru  7779  ltexprlemell  7808  ltexprlemelu  7809  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  ltexpri  7823  recexprlemm  7834  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  recexpr  7848  addclsr  7963  mulclsr  7964  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  suplocsr  8019  pitonn  8058  peano2nnnn  8063  axaddrcl  8075  axmulrcl  8077  peano5nnnn  8102  axpre-suploclemres  8111  negreb  8434  negf1o  8551  eqord1  8653  eqord2  8654  cju  9131  peano2nn  9145  nn1m1nn  9151  nnaddcl  9153  nnmulcl  9154  nnsub  9172  nndivtr  9175  un0addcl  9425  un0mulcl  9426  elnnnn0  9435  elz  9471  nnnegz  9472  znegclb  9502  zaddcllempos  9506  zaddcllemneg  9508  zaddcl  9509  nzadd  9522  zmulcl  9523  elz2  9541  zneo  9571  nneoor  9572  zeo  9575  peano5uzti  9578  zindd  9588  uzp1  9780  uzaddcl  9810  supinfneg  9819  infsupneg  9820  supminfex  9821  ublbneg  9837  eqreznegel  9838  negm  9839  qmulz  9847  qnegcl  9860  irradd  9870  irrmul  9871  fzrev2  10310  infssuzex  10483  infssuzcldc  10485  zsupssdc  10488  negqmod0  10583  frec2uzuzd  10654  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgsuctlem  10675  xnn0nnen  10689  iseqovex  10710  seq3val  10712  seqvalcd  10713  seq3-1  10714  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3clss  10723  monoord  10737  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seqf1og  10773  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  ser3ge0  10788  expp1  10798  expcllem  10802  expcl2lemap  10803  m1expcl2  10813  facnn  10979  fac0  10980  fac1  10981  faccl  10987  facdiv  10990  facndiv  10991  bccmpl  11006  bcn2  11016  bccl  11019  fihasheqf1oi  11039  seq3coll  11096  ccatalpha  11180  reuccatpfxs1lem  11317  reuccatpfxs1  11318  shftlem  11367  shftf  11381  seq3shft  11389  cjval  11396  cjth  11397  remim  11411  uzin2  11538  caubnd2  11668  negfi  11779  xrmaxltsup  11809  clim  11832  clim2  11834  climshftlemg  11853  climcn1  11859  climcn2  11860  iserex  11890  climub  11895  climserle  11896  climcau  11898  serf0  11903  sumfct  11925  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  fsumf1o  11941  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumsplitf  11959  sumpr  11964  sumtp  11965  fsumm1  11967  fsum1p  11969  isummulc2  11977  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fisum0diag2  11998  fsummulc2  11999  fsumge1  12012  fsum00  12013  fsumabs  12016  telfsumo  12017  telfsumo2  12018  fsumparts  12021  fsumrelem  12022  fsumiun  12028  binomlem  12034  isumshft  12041  isum1p  12043  isumrpcl  12045  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslem2  12087  mertensabs  12088  clim2prod  12090  prodfap0  12096  prodfrecap  12097  prodfdivap  12098  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  prodfct  12138  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  fprodm1  12149  fprod1p  12150  fprodm1s  12152  fprodp1s  12153  fprodcl2lem  12156  fprodabs  12167  fprod2dlemstep  12173  fprodcnv  12176  fprodcom2fi  12177  fprodrec  12180  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  fprodle  12191  zeo3  12419  mulsucdiv2z  12436  zob  12442  nn0o1gt2  12456  nno  12457  nn0o  12458  uzwodc  12598  qnumdencl  12749  pcqcl  12869  pcxnn0cl  12873  pcxcl  12874  pcgcd1  12891  dvdsprmpweqle  12900  pcmpt  12906  pcmpt2  12907  pcmptdvds  12908  infpnlem2  12923  1arith  12930  elgz  12934  mul4sq  12957  4sqlem13m  12966  4sqlem17  12970  4sqlem18  12971  4sqlem19  12972  znnen  13009  ennnfonelemj0  13012  ennnfonelemg  13014  ennnfonelemom  13019  ctinfom  13039  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  ctiunctlemudc  13048  ctiunctlemfo  13050  ssnnctlemct  13057  infpn2  13067  isstruct2im  13082  isstruct2r  13083  imasaddfnlemg  13387  ercpbl  13404  xpsfrnel2  13419  mgmsscl  13434  mgm1  13443  sgrppropd  13486  mndpropd  13513  issubm  13545  0subm  13557  insubm  13558  mhmima  13564  mulgsubcl  13713  issubg  13750  subgex  13753  issubg2m  13766  issubg4m  13770  0subg  13776  isnsg  13779  isnsg2  13780  nsgbi  13781  isnsg3  13784  elnmz  13785  nmzbi  13786  nmzsubg  13787  nmznsg  13790  releqgg  13797  eqgex  13798  eqgval  13800  eqgid  13803  ghmrn  13834  ghmnsgima  13845  eqgabl  13907  ablnsg  13911  gsumfzmhm2  13921  isrng  13937  issrg  13968  srgfcl  13976  isring  14003  iscrng  14006  dvdsrd  14098  unitsubm  14123  isrim0  14165  issubrng  14203  subrngringnsg  14209  issubrng2  14214  opprsubrngg  14215  issubrg  14225  subrgsubm  14238  subrgugrp  14244  issubrg2  14245  issubrg3  14251  subrgpropd  14257  aprval  14286  aprsym  14288  islmod  14295  lmodlema  14296  islmodd  14297  lmodprop2d  14352  rmodislmodlem  14354  rmodislmod  14355  lsssetm  14360  islssmd  14363  lssclg  14368  lsslss  14385  lsspropdg  14435  islidlm  14483  rnglidlmcl  14484  isridlrng  14486  rnglidlmmgm  14500  isridl  14508  gsumfzfsumlemm  14591  psrbag  14673  psr1clfi  14692  uniopn  14715  inopn  14717  fiinopn  14718  iscld  14817  iuncld  14829  tgrest  14883  iscn  14911  cnpval  14912  iscnp  14913  tgcn  14922  ssidcn  14924  lmbrf  14929  cnpnei  14933  cnima  14934  cnconst2  14947  cnrest2  14950  cnptopresti  14952  cnptoprest  14953  lmres  14962  lmtopcnp  14964  txbasval  14981  tx1cn  14983  tx2cn  14984  txcnp  14985  txcnmpt  14987  txdis1cn  14992  txlm  14993  cnmpt11  14997  cnmpt12  15001  cnmpt21  15005  cnmpt22  15008  ishmeo  15018  hmeoopn  15025  hmeocld  15026  qtopbasss  15235  fsumcncntop  15281  expcn  15283  expcncf  15323  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthdec  15358  limccl  15373  ellimc3apf  15374  cnmptlimc  15388  limccoap  15392  dvmptfsum  15439  plycolemc  15472  plycj  15475  2irrexpq  15690  2irrexpqap  15692  fsumdvdsmul  15705  perfect  15715  lgsval  15723  lgsval2lem  15729  lgsdir2lem4  15750  lgsdir2  15752  m1lgs  15804  2lgs  15823  mul2sq  15835  2sqlem6  15839  wlkcprim  16147  isclwwlk  16189  clwwlk1loop  16194  clwwlkccatlem  16195  clwwlkn1  16213  loopclwwlkn1b  16214  clwwlkn1loopb  16215  clwwlkn2  16216  clwwlkext2edg  16217  umgr2cwwk2dif  16219  s2elclwwlknon2  16231  clwwlknonex2lem2  16233  clwwlknonex2  16234  bdinex1g  16432  bj-intexr  16439  bj-prexg  16442  bj-uniex  16448  bj-uniexg  16449  bdunexb  16451  bj-indsuc  16459  exmidsbthrlem  16562  qdencn  16567  iswomni0  16591