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  4037  breq2  4038  inex1g  4170  intexr  4184  pwexg  4214  prexg  4245  opelopabsb  4295  pofun  4348  seex  4371  uniex  4473  uniexg  4475  unexb  4478  abnexg  4482  reusv3  4496  rabxfrd  4505  onun2  4527  onsucelsucexmid  4567  ordsucunielexmid  4568  dcextest  4618  tfisi  4624  peano2  4632  seinxp  4735  opabid2  4798  opeliunxp2  4807  elrn2g  4857  opeldm  4870  opeldmg  4872  elreldm  4893  elrn2  4909  opelresg  4954  elsnres  4984  iss  4993  elimasng  5038  issref  5053  rnxpid  5105  unielrel  5198  dffun5r  5271  funopg  5293  brprcneu  5554  tz6.12f  5590  fvelrnb  5611  ssimaex  5625  dmfco  5632  fvmpt3  5643  mptfvex  5650  fvmptf  5657  respreima  5693  fvelrn  5696  ffnfvf  5724  ffvresb  5728  fmptco  5731  fmptcof  5732  fsn  5737  fressnfv  5752  fnex  5787  funfvima  5797  funfvima3  5799  f1mpt  5821  fliftfuns  5848  isoselem  5870  ovrspc2v  5951  ffnov  6030  fovcld  6031  ovmpos  6050  ov2gf  6051  ovg  6066  funimassov  6077  caovclg  6080  elovmpo  6126  off  6152  caofdig  6173  fnexALT  6177  focdmex  6181  f1stres  6226  f2ndres  6227  xp1st  6232  xp2nd  6233  elxp6  6236  oprssdmm  6238  unielxp  6241  fmpox  6267  mpofvex  6272  opeliunxp2f  6305  dftpos4  6330  smoel  6367  tfrlem3-2d  6379  tfrlem8  6385  tfrlem9  6386  tfrlemibxssdm  6394  tfrlemi1  6399  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgtfr  6441  rdgon  6453  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecsuclem  6473  nnacl  6547  nnmcl  6548  nnmordi  6583  nnaordex  6595  nnm00  6597  erexb  6626  qliftfuns  6687  ixpsnval  6769  elixp2  6770  resixp  6801  mptelixpg  6802  elixpsn  6803  fundmen  6874  fopwdom  6906  xpf1o  6914  dif1en  6949  diffitest  6957  diffifi  6964  inffiexmid  6976  unfiexmid  6988  unfidisj  6992  prfidceq  6998  fiintim  7001  xpfi  7002  ssfirab  7006  fnfi  7011  iunfidisj  7021  snexxph  7025  fidcenumlemr  7030  elfi2  7047  ctssdccl  7186  isnumi  7262  cc2lem  7351  cc3  7353  addnidpig  7422  indpi  7428  dfplpq2  7440  addclnq  7461  mulclnq  7462  nnnq0lem1  7532  addclnq0  7537  mulclnq0  7538  nqpnq0nq  7539  distrnq0  7545  prloc  7577  prarloclemlo  7580  prarloclem3  7583  prarloclem5  7586  genpml  7603  genpmu  7604  addnqprl  7615  addnqpru  7616  mulnqprl  7654  mulnqpru  7655  ltexprlemell  7684  ltexprlemelu  7685  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  ltexpri  7699  recexprlemm  7710  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  recexpr  7724  addclsr  7839  mulclsr  7840  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  suplocsr  7895  pitonn  7934  peano2nnnn  7939  axaddrcl  7951  axmulrcl  7953  peano5nnnn  7978  axpre-suploclemres  7987  negreb  8310  negf1o  8427  eqord1  8529  eqord2  8530  cju  9007  peano2nn  9021  nn1m1nn  9027  nnaddcl  9029  nnmulcl  9030  nnsub  9048  nndivtr  9051  un0addcl  9301  un0mulcl  9302  elnnnn0  9311  elz  9347  nnnegz  9348  znegclb  9378  zaddcllempos  9382  zaddcllemneg  9384  zaddcl  9385  nzadd  9397  zmulcl  9398  elz2  9416  zneo  9446  nneoor  9447  zeo  9450  peano5uzti  9453  zindd  9463  uzp1  9654  uzaddcl  9679  supinfneg  9688  infsupneg  9689  supminfex  9690  ublbneg  9706  eqreznegel  9707  negm  9708  qmulz  9716  qnegcl  9729  irradd  9739  irrmul  9740  fzrev2  10179  infssuzex  10342  infssuzcldc  10344  zsupssdc  10347  negqmod0  10442  frec2uzuzd  10513  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  frecuzrdgsuctlem  10534  xnn0nnen  10548  iseqovex  10569  seq3val  10571  seqvalcd  10572  seq3-1  10573  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3clss  10582  monoord  10596  monoord2  10597  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seqf1og  10632  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  seq3distr  10643  ser3ge0  10647  expp1  10657  expcllem  10661  expcl2lemap  10662  m1expcl2  10672  facnn  10838  fac0  10839  fac1  10840  faccl  10846  facdiv  10849  facndiv  10850  bccmpl  10865  bcn2  10875  bccl  10878  fihasheqf1oi  10898  seq3coll  10953  shftlem  11000  shftf  11014  seq3shft  11022  cjval  11029  cjth  11030  remim  11044  uzin2  11171  caubnd2  11301  negfi  11412  xrmaxltsup  11442  clim  11465  clim2  11467  climshftlemg  11486  climcn1  11492  climcn2  11493  iserex  11523  climub  11528  climserle  11529  climcau  11531  serf0  11536  sumfct  11558  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsumgcl  11570  fsum3  11571  fsumf1o  11574  isumss  11575  isumss2  11577  fsum3cvg2  11578  fsum3ser  11581  fsumcl2lem  11582  fsumsplitf  11592  sumpr  11597  sumtp  11598  fsumm1  11600  fsum1p  11602  isummulc2  11610  fsum2dlemstep  11618  fisumcom2  11622  fsumshftm  11629  fisum0diag2  11631  fsummulc2  11632  fsumge1  11645  fsum00  11646  fsumabs  11649  telfsumo  11650  telfsumo2  11651  fsumparts  11654  fsumrelem  11655  fsumiun  11661  binomlem  11667  isumshft  11674  isum1p  11676  isumrpcl  11678  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemseq  11710  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  mertenslem2  11720  mertensabs  11721  clim2prod  11723  prodfap0  11729  prodfrecap  11730  prodfdivap  11731  prodrbdclem  11755  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  prodfct  11771  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  fprodm1  11782  fprod1p  11783  fprodm1s  11785  fprodp1s  11786  fprodcl2lem  11789  fprodabs  11800  fprod2dlemstep  11806  fprodcnv  11809  fprodcom2fi  11810  fprodrec  11813  fproddivapf  11815  fprodsplitf  11816  fprodsplit1f  11818  fprodle  11824  zeo3  12052  mulsucdiv2z  12069  zob  12075  nn0o1gt2  12089  nno  12090  nn0o  12091  uzwodc  12231  qnumdencl  12382  pcqcl  12502  pcxnn0cl  12506  pcxcl  12507  pcgcd1  12524  dvdsprmpweqle  12533  pcmpt  12539  pcmpt2  12540  pcmptdvds  12541  infpnlem2  12556  1arith  12563  elgz  12567  mul4sq  12590  4sqlem13m  12599  4sqlem17  12603  4sqlem18  12604  4sqlem19  12605  znnen  12642  ennnfonelemj0  12645  ennnfonelemg  12647  ennnfonelemom  12652  ctinfom  12672  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunctlemfo  12683  ssnnctlemct  12690  infpn2  12700  isstruct2im  12715  isstruct2r  12716  imasaddfnlemg  13018  ercpbl  13035  xpsfrnel2  13050  mgmsscl  13065  mgm1  13074  sgrppropd  13117  mndpropd  13144  issubm  13176  0subm  13188  insubm  13189  mhmima  13195  mulgsubcl  13344  issubg  13381  subgex  13384  issubg2m  13397  issubg4m  13401  0subg  13407  isnsg  13410  isnsg2  13411  nsgbi  13412  isnsg3  13415  elnmz  13416  nmzbi  13417  nmzsubg  13418  nmznsg  13421  releqgg  13428  eqgex  13429  eqgval  13431  eqgid  13434  ghmrn  13465  ghmnsgima  13476  eqgabl  13538  ablnsg  13542  gsumfzmhm2  13552  isrng  13568  issrg  13599  srgfcl  13607  isring  13634  iscrng  13637  dvdsrd  13728  unitsubm  13753  isrim0  13795  issubrng  13833  subrngringnsg  13839  issubrng2  13844  opprsubrngg  13845  issubrg  13855  subrgsubm  13868  subrgugrp  13874  issubrg2  13875  issubrg3  13881  subrgpropd  13887  aprval  13916  aprsym  13918  islmod  13925  lmodlema  13926  islmodd  13927  lmodprop2d  13982  rmodislmodlem  13984  rmodislmod  13985  lsssetm  13990  islssmd  13993  lssclg  13998  lsslss  14015  lsspropdg  14065  islidlm  14113  rnglidlmcl  14114  isridlrng  14116  rnglidlmmgm  14130  isridl  14138  gsumfzfsumlemm  14221  psrbag  14303  psr1clfi  14322  uniopn  14345  inopn  14347  fiinopn  14348  iscld  14447  iuncld  14459  tgrest  14513  iscn  14541  cnpval  14542  iscnp  14543  tgcn  14552  ssidcn  14554  lmbrf  14559  cnpnei  14563  cnima  14564  cnconst2  14577  cnrest2  14580  cnptopresti  14582  cnptoprest  14583  lmres  14592  lmtopcnp  14594  txbasval  14611  tx1cn  14613  tx2cn  14614  txcnp  14615  txcnmpt  14617  txdis1cn  14622  txlm  14623  cnmpt11  14627  cnmpt12  14631  cnmpt21  14635  cnmpt22  14638  ishmeo  14648  hmeoopn  14655  hmeocld  14656  qtopbasss  14865  fsumcncntop  14911  expcn  14913  expcncf  14953  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  ivthinc  14987  ivthdec  14988  limccl  15003  ellimc3apf  15004  cnmptlimc  15018  limccoap  15022  dvmptfsum  15069  plycolemc  15102  plycj  15105  2irrexpq  15320  2irrexpqap  15322  fsumdvdsmul  15335  perfect  15345  lgsval  15353  lgsval2lem  15359  lgsdir2lem4  15380  lgsdir2  15382  m1lgs  15434  2lgs  15453  mul2sq  15465  2sqlem6  15469  bdinex1g  15655  bj-intexr  15662  bj-prexg  15665  bj-uniex  15671  bj-uniexg  15672  bdunexb  15674  bj-indsuc  15682  exmidsbthrlem  15779  qdencn  15784  iswomni0  15808