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  2908  rspcimedv  2909  reuind  3008  sbcel2g  3145  sbccsb2g  3154  breq1  4085  breq2  4086  inex1g  4219  intexr  4233  pwexg  4263  prexg  4294  opelopabsb  4347  pofun  4402  seex  4425  uniex  4527  uniexg  4529  unexb  4532  abnexg  4536  reusv3  4550  rabxfrd  4559  onun2  4581  onsucelsucexmid  4621  ordsucunielexmid  4622  dcextest  4672  tfisi  4678  peano2  4686  seinxp  4789  opabid2  4852  opeliunxp2  4861  elrn2g  4911  opeldm  4925  opeldmg  4927  elreldm  4949  elrn2  4965  opelresg  5011  elsnres  5041  iss  5050  elimasng  5095  issref  5110  rnxpid  5162  unielrel  5255  dffun5r  5329  funopg  5351  brprcneu  5619  tz6.12f  5655  fvelrnb  5680  ssimaex  5694  dmfco  5701  fvmpt3  5712  mptfvex  5719  fvmptf  5726  respreima  5762  fvelrn  5765  ffnfvf  5793  ffvresb  5797  fmptco  5800  fmptcof  5801  fsn  5806  fressnfv  5825  fnex  5860  funfvima  5870  funfvima3  5872  f1mpt  5894  fliftfuns  5921  isoselem  5943  ovrspc2v  6026  ffnov  6107  fovcld  6108  ovmpos  6127  ov2gf  6128  ovg  6143  funimassov  6154  caovclg  6157  elovmpo  6203  off  6229  caofdig  6250  fnexALT  6254  focdmex  6258  f1stres  6303  f2ndres  6304  xp1st  6309  xp2nd  6310  elxp6  6313  oprssdmm  6315  unielxp  6318  fmpox  6344  mpofvex  6349  opeliunxp2f  6382  dftpos4  6407  smoel  6444  tfrlem3-2d  6456  tfrlem8  6462  tfrlem9  6463  tfrlemibxssdm  6471  tfrlemi1  6476  tfrexlem  6478  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemaccex  6492  tfr1onlemres  6493  tfri1dALT  6495  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemaccex  6505  tfrcllemres  6506  tfrcl  6508  rdgtfr  6518  rdgon  6530  frecabex  6542  frecabcl  6543  frecfcllem  6548  frecsuclem  6550  nnacl  6624  nnmcl  6625  nnmordi  6660  nnaordex  6672  nnm00  6674  erexb  6703  qliftfuns  6764  ixpsnval  6846  elixp2  6847  resixp  6878  mptelixpg  6879  elixpsn  6880  fundmen  6957  fopwdom  6993  xpf1o  7001  dif1en  7037  diffitest  7045  diffifi  7052  inffiexmid  7064  unfiexmid  7076  unfidisj  7080  prfidceq  7086  fiintim  7089  xpfi  7090  ssfirab  7094  fnfi  7099  iunfidisj  7109  snexxph  7113  fidcenumlemr  7118  elfi2  7135  ctssdccl  7274  isnumi  7350  cc2lem  7448  cc3  7450  addnidpig  7519  indpi  7525  dfplpq2  7537  addclnq  7558  mulclnq  7559  nnnq0lem1  7629  addclnq0  7634  mulclnq0  7635  nqpnq0nq  7636  distrnq0  7642  prloc  7674  prarloclemlo  7677  prarloclem3  7680  prarloclem5  7683  genpml  7700  genpmu  7701  addnqprl  7712  addnqpru  7713  mulnqprl  7751  mulnqpru  7752  ltexprlemell  7781  ltexprlemelu  7782  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  ltexpri  7796  recexprlemm  7807  recexprlemdisj  7813  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  recexpr  7821  addclsr  7936  mulclsr  7937  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  suplocsr  7992  pitonn  8031  peano2nnnn  8036  axaddrcl  8048  axmulrcl  8050  peano5nnnn  8075  axpre-suploclemres  8084  negreb  8407  negf1o  8524  eqord1  8626  eqord2  8627  cju  9104  peano2nn  9118  nn1m1nn  9124  nnaddcl  9126  nnmulcl  9127  nnsub  9145  nndivtr  9148  un0addcl  9398  un0mulcl  9399  elnnnn0  9408  elz  9444  nnnegz  9445  znegclb  9475  zaddcllempos  9479  zaddcllemneg  9481  zaddcl  9482  nzadd  9495  zmulcl  9496  elz2  9514  zneo  9544  nneoor  9545  zeo  9548  peano5uzti  9551  zindd  9561  uzp1  9752  uzaddcl  9777  supinfneg  9786  infsupneg  9787  supminfex  9788  ublbneg  9804  eqreznegel  9805  negm  9806  qmulz  9814  qnegcl  9827  irradd  9837  irrmul  9838  fzrev2  10277  infssuzex  10448  infssuzcldc  10450  zsupssdc  10453  negqmod0  10548  frec2uzuzd  10619  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  frecuzrdgsuctlem  10640  xnn0nnen  10654  iseqovex  10675  seq3val  10677  seqvalcd  10678  seq3-1  10679  seqf  10681  seq3p1  10682  seqovcd  10684  seqp1cd  10687  seq3clss  10688  monoord  10702  monoord2  10703  ser3mono  10704  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seq3caopr2  10710  seqcaopr2g  10711  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1oleml  10733  seq3f1o  10734  seqf1og  10738  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  seq3distr  10749  ser3ge0  10753  expp1  10763  expcllem  10767  expcl2lemap  10768  m1expcl2  10778  facnn  10944  fac0  10945  fac1  10946  faccl  10952  facdiv  10955  facndiv  10956  bccmpl  10971  bcn2  10981  bccl  10984  fihasheqf1oi  11004  seq3coll  11059  reuccatpfxs1lem  11273  reuccatpfxs1  11274  shftlem  11322  shftf  11336  seq3shft  11344  cjval  11351  cjth  11352  remim  11366  uzin2  11493  caubnd2  11623  negfi  11734  xrmaxltsup  11764  clim  11787  clim2  11789  climshftlemg  11808  climcn1  11814  climcn2  11815  iserex  11845  climub  11850  climserle  11851  climcau  11853  serf0  11858  sumfct  11880  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  fsumf1o  11896  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumsplitf  11914  sumpr  11919  sumtp  11920  fsumm1  11922  fsum1p  11924  isummulc2  11932  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fisum0diag2  11953  fsummulc2  11954  fsumge1  11967  fsum00  11968  fsumabs  11971  telfsumo  11972  telfsumo2  11973  fsumparts  11976  fsumrelem  11977  fsumiun  11983  binomlem  11989  isumshft  11996  isum1p  11998  isumrpcl  12000  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemseq  12032  cvgratnnlemabsle  12033  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  mertenslem2  12042  mertensabs  12043  clim2prod  12045  prodfap0  12051  prodfrecap  12052  prodfdivap  12053  prodrbdclem  12077  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  prodfct  12093  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodmul  12097  fprodm1  12104  fprod1p  12105  fprodm1s  12107  fprodp1s  12108  fprodcl2lem  12111  fprodabs  12122  fprod2dlemstep  12128  fprodcnv  12131  fprodcom2fi  12132  fprodrec  12135  fproddivapf  12137  fprodsplitf  12138  fprodsplit1f  12140  fprodle  12146  zeo3  12374  mulsucdiv2z  12391  zob  12397  nn0o1gt2  12411  nno  12412  nn0o  12413  uzwodc  12553  qnumdencl  12704  pcqcl  12824  pcxnn0cl  12828  pcxcl  12829  pcgcd1  12846  dvdsprmpweqle  12855  pcmpt  12861  pcmpt2  12862  pcmptdvds  12863  infpnlem2  12878  1arith  12885  elgz  12889  mul4sq  12912  4sqlem13m  12921  4sqlem17  12925  4sqlem18  12926  4sqlem19  12927  znnen  12964  ennnfonelemj0  12967  ennnfonelemg  12969  ennnfonelemom  12974  ctinfom  12994  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  ctiunctlemudc  13003  ctiunctlemfo  13005  ssnnctlemct  13012  infpn2  13022  isstruct2im  13037  isstruct2r  13038  imasaddfnlemg  13342  ercpbl  13359  xpsfrnel2  13374  mgmsscl  13389  mgm1  13398  sgrppropd  13441  mndpropd  13468  issubm  13500  0subm  13512  insubm  13513  mhmima  13519  mulgsubcl  13668  issubg  13705  subgex  13708  issubg2m  13721  issubg4m  13725  0subg  13731  isnsg  13734  isnsg2  13735  nsgbi  13736  isnsg3  13739  elnmz  13740  nmzbi  13741  nmzsubg  13742  nmznsg  13745  releqgg  13752  eqgex  13753  eqgval  13755  eqgid  13758  ghmrn  13789  ghmnsgima  13800  eqgabl  13862  ablnsg  13866  gsumfzmhm2  13876  isrng  13892  issrg  13923  srgfcl  13931  isring  13958  iscrng  13961  dvdsrd  14052  unitsubm  14077  isrim0  14119  issubrng  14157  subrngringnsg  14163  issubrng2  14168  opprsubrngg  14169  issubrg  14179  subrgsubm  14192  subrgugrp  14198  issubrg2  14199  issubrg3  14205  subrgpropd  14211  aprval  14240  aprsym  14242  islmod  14249  lmodlema  14250  islmodd  14251  lmodprop2d  14306  rmodislmodlem  14308  rmodislmod  14309  lsssetm  14314  islssmd  14317  lssclg  14322  lsslss  14339  lsspropdg  14389  islidlm  14437  rnglidlmcl  14438  isridlrng  14440  rnglidlmmgm  14454  isridl  14462  gsumfzfsumlemm  14545  psrbag  14627  psr1clfi  14646  uniopn  14669  inopn  14671  fiinopn  14672  iscld  14771  iuncld  14783  tgrest  14837  iscn  14865  cnpval  14866  iscnp  14867  tgcn  14876  ssidcn  14878  lmbrf  14883  cnpnei  14887  cnima  14888  cnconst2  14901  cnrest2  14904  cnptopresti  14906  cnptoprest  14907  lmres  14916  lmtopcnp  14918  txbasval  14935  tx1cn  14937  tx2cn  14938  txcnp  14939  txcnmpt  14941  txdis1cn  14946  txlm  14947  cnmpt11  14951  cnmpt12  14955  cnmpt21  14959  cnmpt22  14962  ishmeo  14972  hmeoopn  14979  hmeocld  14980  qtopbasss  15189  fsumcncntop  15235  expcn  15237  expcncf  15277  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  ivthinc  15311  ivthdec  15312  limccl  15327  ellimc3apf  15328  cnmptlimc  15342  limccoap  15346  dvmptfsum  15393  plycolemc  15426  plycj  15429  2irrexpq  15644  2irrexpqap  15646  fsumdvdsmul  15659  perfect  15669  lgsval  15677  lgsval2lem  15683  lgsdir2lem4  15704  lgsdir2  15706  m1lgs  15758  2lgs  15777  mul2sq  15789  2sqlem6  15793  bdinex1g  16222  bj-intexr  16229  bj-prexg  16232  bj-uniex  16238  bj-uniexg  16239  bdunexb  16241  bj-indsuc  16249  exmidsbthrlem  16349  qdencn  16354  iswomni0  16378