Theorem eleq1d 2307

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12d  2309  eqeltrd  2315  eqneltrd  2334  eqneltrrd  2335  rspcimdv  2930  rspcimedv  2931  reuind  3031  sbcel2g  3168  sbccsb2g  3177  breq1  4133  breq2  4134  inex1g  4269  intexr  4286  pwexg  4317  prexg  4349  opelopabsb  4402  pofun  4457  seex  4480  uniex  4583  uniexg  4585  unexb  4588  abnexg  4592  reusv3  4606  rabxfrd  4615  onun2  4637  onsucelsucexmid  4677  ordsucunielexmid  4678  dcextest  4728  tfisi  4734  peano2  4742  seinxp  4846  opabid2  4911  opeliunxp2  4920  elrn2g  4970  opeldm  4984  opeldmg  4986  elreldm  5008  elrn2  5024  opelresg  5070  elsnres  5100  iss  5109  xpexcnvm  5142  elimasng  5155  issref  5170  rnxpid  5222  unielrel  5315  dffun5r  5389  funopg  5411  brprcneu  5688  tz6.12f  5724  fvelrnb  5750  ssimaex  5764  dmfco  5773  fvmpt3  5784  mptfvex  5791  fvmptf  5798  respreima  5836  fvelrn  5839  ffnfvf  5867  ffvresb  5871  fmptco  5874  fmptcof  5875  fsn  5880  fsn2g  5883  fressnfv  5902  fnex  5937  funfvima  5950  funfvima3  5952  f1mpt  5977  fliftfuns  6004  isoselem  6026  ovrspc2v  6111  ffnov  6192  fovcld  6193  ovmpos  6212  ov2gf  6213  ovg  6228  funimassov  6239  caovclg  6242  elovmpo  6288  off  6315  caofdig  6336  fnexALT  6340  focdmex  6344  f1stres  6393  f2ndres  6394  xp1st  6399  xp2nd  6400  elxp6  6403  oprssdmm  6405  unielxp  6408  fmpox  6436  mpofvex  6441  elmpom  6474  suppofss1dcl  6504  suppofss2dcl  6505  opeliunxp2f  6509  dftpos4  6534  smoel  6571  tfrlem3-2d  6583  tfrlem8  6589  tfrlem9  6590  tfrlemibxssdm  6598  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgtfr  6645  rdgon  6657  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecsuclem  6677  nnacl  6753  nnmcl  6754  nnmordi  6789  nnaordex  6801  nnm00  6803  erexb  6832  qliftfuns  6893  ixpsnval  6983  elixp2  6984  resixp  7015  mptelixpg  7016  elixpsn  7017  fundmen  7094  fopwdom  7136  xpf1o  7144  dif1en  7183  diffitest  7191  diffifi  7198  inffiexmid  7213  unfiexmid  7225  unfidisj  7229  prfidceq  7235  fiintim  7238  xpfi  7239  ssfirab  7244  fnfi  7250  iunfidisj  7260  mapfi  7261  snexxph  7267  fidcenumlemr  7272  isfsupp  7289  ffsuppbi  7300  elfi2  7306  ctssdccl  7451  isnumi  7527  cc2lem  7632  cc3  7634  addnidpig  7703  indpi  7709  dfplpq2  7721  addclnq  7742  mulclnq  7743  nnnq0lem1  7813  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  distrnq0  7826  prloc  7858  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  ltexprlemell  7965  ltexprlemelu  7966  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  ltexpri  7980  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  addclsr  8120  mulclsr  8121  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  suplocsr  8176  pitonn  8215  peano2nnnn  8220  axaddrcl  8232  axmulrcl  8234  peano5nnnn  8259  axpre-suploclemres  8268  negreb  8591  negf1o  8709  eqord1  8811  eqord2  8812  cju  9291  indfval  9299  peano2nn  9316  nn1m1nn  9322  nnaddcl  9324  nnmulcl  9325  nnsub  9343  nndivtr  9346  un0addcl  9596  un0mulcl  9597  elnnnn0  9606  fcdmnn0fsuppg  9618  elz  9646  nnnegz  9647  znegclb  9677  zaddcllempos  9681  zaddcllemneg  9683  zaddcl  9684  nzadd  9697  zmulcl  9698  elz2  9716  zneo  9747  nneoor  9748  zeo  9751  peano5uzti  9754  zindd  9764  uzp1  9956  uzaddcl  9986  supinfneg  9995  infsupneg  9996  supminfex  9997  ublbneg  10013  eqreznegel  10014  negm  10015  qmulz  10023  qnegcl  10036  irradd  10046  irrmul  10047  fzsplit3  10458  fzspl  10476  fzrev2  10492  infssuzex  10666  infssuzcldc  10668  zsupssdc  10673  negqmod0  10768  frec2uzuzd  10839  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgsuctlem  10860  xnn0nnen  10874  iseqovex  10895  seq3val  10897  seqvalcd  10898  seq3-1  10899  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3clss  10908  monoord  10922  monoord2  10923  ser3mono  10924  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  seqf1og  10958  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  ser3ge0  10973  expp1  10983  expcllem  10987  expcl2lemap  10988  m1expcl2  10998  facnn  11165  fac0  11166  fac1  11167  faccl  11173  facdiv  11176  facndiv  11177  bccmpl  11192  bcn2  11202  bccl  11205  fihasheqf1oi  11226  hashf1lem2  11286  seq3coll  11294  ccatalpha  11381  reuccatpfxs1lem  11518  reuccatpfxs1  11519  shftlem  11581  shftf  11595  seq3shft  11603  cjval  11610  cjth  11611  remim  11625  uzin2  11753  caubnd2  11883  negfi  11994  xrmaxltsup  12024  clim  12047  clim2  12049  climshftlemg  12068  climcn1  12074  climcn2  12075  iserex  12105  climub  12110  climserle  12111  climcau  12113  serf0  12118  sumfct  12140  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  zsumdc  12151  fsumgcl  12153  fsum3  12154  fsumf1o  12157  isumss  12158  isumss2  12160  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumsplitf  12175  sumpr  12180  sumtp  12181  fsumm1  12183  fsum1p  12185  isummulc2  12193  fsum2dlemstep  12201  fisumcom2  12205  fsumshftm  12212  fisum0diag2  12214  fsummulc2  12215  fsumge1  12228  fsum00  12229  fsumabs  12232  telfsumo  12233  telfsumo2  12234  fsumparts  12237  fsumrelem  12238  fsumiun  12244  binomlem  12250  isumshft  12257  isum1p  12259  isumrpcl  12261  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  cvgratz  12299  mertenslem2  12303  mertensabs  12304  clim2prod  12306  prodfap0  12312  prodfrecap  12313  prodfdivap  12314  prodrbdclem  12338  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  prodfct  12354  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodmul  12358  fprodm1  12365  fprod1p  12366  fprodm1s  12368  fprodp1s  12369  fprodcl2lem  12372  fprodabs  12383  fprod2dlemstep  12389  fprodcnv  12392  fprodcom2fi  12393  fprodrec  12396  fproddivapf  12398  fprodsplitf  12399  fprodsplit1f  12401  fprodle  12407  zeo3  12635  mulsucdiv2z  12652  zob  12658  nn0o1gt2  12672  nno  12673  nn0o  12674  uzwodc  12814  qnumdencl  12965  pcqcl  13085  pcxnn0cl  13089  pcxcl  13090  pcgcd1  13107  dvdsprmpweqle  13116  pcmpt  13122  pcmpt2  13123  pcmptdvds  13124  infpnlem2  13139  1arith  13146  elgz  13150  mul4sq  13173  4sqlem13m  13182  4sqlem17  13186  4sqlem18  13187  4sqlem19  13188  ballotfilemsdom  13255  ballotfilemrv  13263  ballotfilemrv1  13264  ballotfilemrv2  13265  ballotfilem1ri  13278  znnen  13289  ennnfonelemj0  13292  ennnfonelemg  13294  ennnfonelemom  13299  ctinfom  13319  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunctlemfo  13330  ssnnctlemct  13337  infpn2  13347  isstruct2im  13362  isstruct2r  13363  imasaddfnlemg  13635  ercpbl  13652  xpsfrnel2  13667  mgmsscl  13681  mgm1  13690  sgrppropd  13728  mndpropd  13753  issubm  13779  0subm  13791  insubm  13792  mhmima  13798  mulgsubcl  13939  issubg  13976  subgex  13979  issubg2m  13992  issubg4m  13996  0subg  14002  isnsg  14005  isnsg2  14006  nsgbi  14007  isnsg3  14010  elnmz  14011  nmzbi  14012  nmzsubg  14013  nmznsg  14016  releqgg  14023  eqgex  14024  eqgval  14026  eqgid  14029  ghmrn  14060  ghmnsgima  14071  eqgabl  14134  ablnsg  14138  gzsummhm2  14146  gsumvalfi  14152  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsummhm2fi  14165  isrng  14233  issrg  14269  srgfcl  14277  isring  14304  iscrng  14307  dvdsrd  14401  unitsubm  14426  isrim0  14468  issubrng  14507  subrngringnsg  14513  issubrng2  14518  opprsubrngg  14519  issubrg  14529  subrgsubm  14542  subrgugrp  14548  issubrg2  14549  issubrg3  14555  subrgpropd  14561  aprval  14591  aprunit  14592  aprsym  14596  opprdrng  14620  islmod  14627  lmodlema  14628  islmodd  14629  lmodprop2d  14685  rmodislmodlem  14687  rmodislmod  14688  lsssetm  14693  islssmd  14696  lssclg  14701  lsslss  14718  lsspropdg  14768  islidlm  14816  rnglidlmcl  14817  isridlrng  14819  rnglidlmmgm  14833  isridl  14841  gsumfsum  14923  psrbag  15053  psr1clfi  15079  uniopn  15102  inopn  15104  fiinopn  15105  iscld  15204  iuncld  15216  tgrest  15270  iscn  15298  cnpval  15299  iscnp  15300  tgcn  15309  ssidcn  15311  lmbrf  15316  cnpnei  15320  cnima  15321  cnconst2  15334  cnrest2  15337  cnptopresti  15339  cnptoprest  15340  lmres  15349  lmtopcnp  15351  txbasval  15368  tx1cn  15370  tx2cn  15371  txcnp  15372  txcnmpt  15374  txdis1cn  15379  txlm  15380  cnmpt11  15384  cnmpt12  15388  cnmpt21  15392  cnmpt22  15395  ishmeo  15405  hmeoopn  15412  hmeocld  15413  qtopbasss  15622  fsumcncntop  15668  expcn  15670  expcncf  15710  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthdec  15745  limccl  15760  ellimc3apf  15761  cnmptlimc  15775  limccoap  15779  dvmptfsum  15826  plycolemc  15859  plycj  15862  2irrexpq  16078  2irrexpqap  16080  pellexlem1  16091  fsumdvdsmul  16105  perfect  16115  lgsval  16123  lgsval2lem  16129  lgsdir2lem4  16150  lgsdir2  16152  m1lgs  16204  2lgs  16223  mul2sq  16235  2sqlem6  16239  wlkcprim  16591  isclwwlk  16635  clwwlk1loop  16640  clwwlkccatlem  16641  clwwlkn1  16659  loopclwwlkn1b  16660  clwwlkn1loopb  16661  clwwlkn2  16662  clwwlkext2edg  16663  umgr2cwwk2dif  16665  s2elclwwlknon2  16677  clwwlknonex2lem2  16679  clwwlknonex2  16680  eupth2lem2dc  16700  eulerpathprum  16721  bdinex1g  16927  bj-intexr  16934  bj-prexg  16937  bj-uniex  16943  bj-uniexg  16944  bdunexb  16946  bj-indsuc  16954  wexmiddiffilem  17043  wexmiddifxy  17046  exmidsbthrlem  17067  qdencn  17072  repiecef  17077  iswomni0  17101