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 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  eleq12d  2309  eqeltrd  2315  eqneltrd  2334  eqneltrrd  2335  rspcimdv  2930  rspcimedv  2931  reuind  3031  sbcel2g  3168  sbccsb2g  3177  breq1  4128  breq2  4129  inex1g  4264  intexr  4281  pwexg  4312  prexg  4344  opelopabsb  4397  pofun  4452  seex  4475  uniex  4578  uniexg  4580  unexb  4583  abnexg  4587  reusv3  4601  rabxfrd  4610  onun2  4632  onsucelsucexmid  4672  ordsucunielexmid  4673  dcextest  4723  tfisi  4729  peano2  4737  seinxp  4841  opabid2  4906  opeliunxp2  4915  elrn2g  4965  opeldm  4979  opeldmg  4981  elreldm  5003  elrn2  5019  opelresg  5065  elsnres  5095  iss  5104  xpexcnvm  5137  elimasng  5150  issref  5165  rnxpid  5217  unielrel  5310  dffun5r  5384  funopg  5406  brprcneu  5683  tz6.12f  5719  fvelrnb  5744  ssimaex  5758  dmfco  5767  fvmpt3  5778  mptfvex  5785  fvmptf  5792  respreima  5827  fvelrn  5830  ffnfvf  5858  ffvresb  5862  fmptco  5865  fmptcof  5866  fsn  5871  fsn2g  5874  fressnfv  5893  fnex  5928  funfvima  5940  funfvima3  5942  f1mpt  5967  fliftfuns  5994  isoselem  6016  ovrspc2v  6101  ffnov  6182  fovcld  6183  ovmpos  6202  ov2gf  6203  ovg  6218  funimassov  6229  caovclg  6232  elovmpo  6278  off  6305  caofdig  6326  fnexALT  6330  focdmex  6334  f1stres  6383  f2ndres  6384  xp1st  6389  xp2nd  6390  elxp6  6393  oprssdmm  6395  unielxp  6398  fmpox  6426  mpofvex  6431  elmpom  6464  suppofss1dcl  6494  suppofss2dcl  6495  opeliunxp2f  6499  dftpos4  6524  smoel  6561  tfrlem3-2d  6573  tfrlem8  6579  tfrlem9  6580  tfrlemibxssdm  6588  tfrlemi1  6593  tfrexlem  6595  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  tfri1dALT  6612  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  rdgtfr  6635  rdgon  6647  frecabex  6659  frecabcl  6660  frecfcllem  6665  frecsuclem  6667  nnacl  6743  nnmcl  6744  nnmordi  6779  nnaordex  6791  nnm00  6793  erexb  6822  qliftfuns  6883  ixpsnval  6973  elixp2  6974  resixp  7005  mptelixpg  7006  elixpsn  7007  fundmen  7084  fopwdom  7126  xpf1o  7134  dif1en  7173  diffitest  7181  diffifi  7188  inffiexmid  7203  unfiexmid  7215  unfidisj  7219  prfidceq  7225  fiintim  7228  xpfi  7229  ssfirab  7234  fnfi  7240  iunfidisj  7250  mapfi  7251  snexxph  7257  fidcenumlemr  7262  isfsupp  7279  ffsuppbi  7290  elfi2  7296  ctssdccl  7441  isnumi  7517  cc2lem  7622  cc3  7624  addnidpig  7693  indpi  7699  dfplpq2  7711  addclnq  7732  mulclnq  7733  nnnq0lem1  7803  addclnq0  7808  mulclnq0  7809  nqpnq0nq  7810  distrnq0  7816  prloc  7848  prarloclemlo  7851  prarloclem3  7854  prarloclem5  7857  genpml  7874  genpmu  7875  addnqprl  7886  addnqpru  7887  mulnqprl  7925  mulnqpru  7926  ltexprlemell  7955  ltexprlemelu  7956  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  ltexpri  7970  recexprlemm  7981  recexprlemdisj  7987  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  recexpr  7995  addclsr  8110  mulclsr  8111  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  suplocsr  8166  pitonn  8205  peano2nnnn  8210  axaddrcl  8222  axmulrcl  8224  peano5nnnn  8249  axpre-suploclemres  8258  negreb  8581  negf1o  8699  eqord1  8801  eqord2  8802  cju  9281  peano2nn  9295  nn1m1nn  9301  nnaddcl  9303  nnmulcl  9304  nnsub  9322  nndivtr  9325  un0addcl  9575  un0mulcl  9576  elnnnn0  9585  fcdmnn0fsuppg  9597  elz  9625  nnnegz  9626  znegclb  9656  zaddcllempos  9660  zaddcllemneg  9662  zaddcl  9663  nzadd  9676  zmulcl  9677  elz2  9695  zneo  9726  nneoor  9727  zeo  9730  peano5uzti  9733  zindd  9743  uzp1  9935  uzaddcl  9965  supinfneg  9974  infsupneg  9975  supminfex  9976  ublbneg  9992  eqreznegel  9993  negm  9994  qmulz  10002  qnegcl  10015  irradd  10025  irrmul  10026  fzsplit3  10436  fzspl  10454  fzrev2  10470  infssuzex  10644  infssuzcldc  10646  zsupssdc  10651  negqmod0  10746  frec2uzuzd  10817  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  xnn0nnen  10852  iseqovex  10873  seq3val  10875  seqvalcd  10876  seq3-1  10877  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3clss  10886  monoord  10900  monoord2  10901  ser3mono  10902  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seq3caopr2  10908  seqcaopr2g  10909  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seq3f1oleml  10931  seq3f1o  10932  seqf1og  10936  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  seq3distr  10947  ser3ge0  10951  expp1  10961  expcllem  10965  expcl2lemap  10966  m1expcl2  10976  facnn  11143  fac0  11144  fac1  11145  faccl  11151  facdiv  11154  facndiv  11155  bccmpl  11170  bcn2  11180  bccl  11183  fihasheqf1oi  11204  hashf1lem2  11264  seq3coll  11272  ccatalpha  11359  reuccatpfxs1lem  11496  reuccatpfxs1  11497  shftlem  11559  shftf  11573  seq3shft  11581  cjval  11588  cjth  11589  remim  11603  uzin2  11731  caubnd2  11861  negfi  11972  xrmaxltsup  12002  clim  12025  clim2  12027  climshftlemg  12046  climcn1  12052  climcn2  12053  iserex  12083  climub  12088  climserle  12089  climcau  12091  serf0  12096  sumfct  12118  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  fsumf1o  12135  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsum3ser  12142  fsumcl2lem  12143  fsumsplitf  12153  sumpr  12158  sumtp  12159  fsumm1  12161  fsum1p  12163  isummulc2  12171  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fisum0diag2  12192  fsummulc2  12193  fsumge1  12206  fsum00  12207  fsumabs  12210  telfsumo  12211  telfsumo2  12212  fsumparts  12215  fsumrelem  12216  fsumiun  12222  binomlem  12228  isumshft  12235  isum1p  12237  isumrpcl  12239  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  cvgratz  12277  mertenslem2  12281  mertensabs  12282  clim2prod  12284  prodfap0  12290  prodfrecap  12291  prodfdivap  12292  prodrbdclem  12316  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  prodfct  12332  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  fprodm1  12343  fprod1p  12344  fprodm1s  12346  fprodp1s  12347  fprodcl2lem  12350  fprodabs  12361  fprod2dlemstep  12367  fprodcnv  12370  fprodcom2fi  12371  fprodrec  12374  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  fprodle  12385  zeo3  12613  mulsucdiv2z  12630  zob  12636  nn0o1gt2  12650  nno  12651  nn0o  12652  uzwodc  12792  qnumdencl  12943  pcqcl  13063  pcxnn0cl  13067  pcxcl  13068  pcgcd1  13085  dvdsprmpweqle  13094  pcmpt  13100  pcmpt2  13101  pcmptdvds  13102  infpnlem2  13117  1arith  13124  elgz  13128  mul4sq  13151  4sqlem13m  13160  4sqlem17  13164  4sqlem18  13165  4sqlem19  13166  ballotfilemsdom  13233  ballotfilemrv  13241  ballotfilemrv1  13242  ballotfilemrv2  13243  ballotfilem1ri  13256  znnen  13267  ennnfonelemj0  13270  ennnfonelemg  13272  ennnfonelemom  13277  ctinfom  13297  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunctlemfo  13308  ssnnctlemct  13315  infpn2  13325  isstruct2im  13340  isstruct2r  13341  imasaddfnlemg  13612  ercpbl  13629  xpsfrnel2  13644  mgmsscl  13658  mgm1  13667  sgrppropd  13705  mndpropd  13730  issubm  13756  0subm  13768  insubm  13769  mhmima  13775  mulgsubcl  13916  issubg  13953  subgex  13956  issubg2m  13969  issubg4m  13973  0subg  13979  isnsg  13982  isnsg2  13983  nsgbi  13984  isnsg3  13987  elnmz  13988  nmzbi  13989  nmzsubg  13990  nmznsg  13993  releqgg  14000  eqgex  14001  eqgval  14003  eqgid  14006  ghmrn  14037  ghmnsgima  14048  eqgabl  14111  ablnsg  14115  gzsummhm2  14123  gsumvalfi  14129  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  gsummhm2fi  14142  isrng  14208  issrg  14243  srgfcl  14251  isring  14278  iscrng  14281  dvdsrd  14374  unitsubm  14399  isrim0  14441  issubrng  14480  subrngringnsg  14486  issubrng2  14491  opprsubrngg  14492  issubrg  14502  subrgsubm  14515  subrgugrp  14521  issubrg2  14522  issubrg3  14528  subrgpropd  14534  aprval  14564  aprunit  14565  aprsym  14569  opprdrng  14593  islmod  14600  lmodlema  14601  islmodd  14602  lmodprop2d  14657  rmodislmodlem  14659  rmodislmod  14660  lsssetm  14665  islssmd  14668  lssclg  14673  lsslss  14690  lsspropdg  14740  islidlm  14788  rnglidlmcl  14789  isridlrng  14791  rnglidlmmgm  14805  isridl  14813  gsumfsum  14895  psrbag  14976  psr1clfi  15002  uniopn  15025  inopn  15027  fiinopn  15028  iscld  15127  iuncld  15139  tgrest  15193  iscn  15221  cnpval  15222  iscnp  15223  tgcn  15232  ssidcn  15234  lmbrf  15239  cnpnei  15243  cnima  15244  cnconst2  15257  cnrest2  15260  cnptopresti  15262  cnptoprest  15263  lmres  15272  lmtopcnp  15274  txbasval  15291  tx1cn  15293  tx2cn  15294  txcnp  15295  txcnmpt  15297  txdis1cn  15302  txlm  15303  cnmpt11  15307  cnmpt12  15311  cnmpt21  15315  cnmpt22  15318  ishmeo  15328  hmeoopn  15335  hmeocld  15336  qtopbasss  15545  fsumcncntop  15591  expcn  15593  expcncf  15633  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthdec  15668  limccl  15683  ellimc3apf  15684  cnmptlimc  15698  limccoap  15702  dvmptfsum  15749  plycolemc  15782  plycj  15785  2irrexpq  16001  2irrexpqap  16003  pellexlem1  16005  fsumdvdsmul  16019  perfect  16029  lgsval  16037  lgsval2lem  16043  lgsdir2lem4  16064  lgsdir2  16066  m1lgs  16118  2lgs  16137  mul2sq  16149  2sqlem6  16153  wlkcprim  16505  isclwwlk  16549  clwwlk1loop  16554  clwwlkccatlem  16555  clwwlkn1  16573  loopclwwlkn1b  16574  clwwlkn1loopb  16575  clwwlkn2  16576  clwwlkext2edg  16577  umgr2cwwk2dif  16579  s2elclwwlknon2  16591  clwwlknonex2lem2  16593  clwwlknonex2  16594  eupth2lem2dc  16614  eulerpathprum  16635  bdinex1g  16841  bj-intexr  16848  bj-prexg  16851  bj-uniex  16857  bj-uniexg  16858  bdunexb  16860  bj-indsuc  16868  exmidsbthrlem  16972  qdencn  16977  repiecef  16982  iswomni0  17006