Theorem eleq1d 2246

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eqeltrd  2254  eqneltrd  2273  eqneltrrd  2274  rspcimdv  2844  rspcimedv  2845  reuind  2944  sbcel2g  3080  sbccsb2g  3089  breq1  4008  breq2  4009  inex1g  4141  intexr  4152  pwexg  4182  prexg  4213  opelopabsb  4262  pofun  4314  seex  4337  uniex  4439  uniexg  4441  unexb  4444  abnexg  4448  reusv3  4462  rabxfrd  4471  onun2  4491  onsucelsucexmid  4531  ordsucunielexmid  4532  dcextest  4582  tfisi  4588  peano2  4596  seinxp  4699  opabid2  4760  opeliunxp2  4769  elrn2g  4819  opeldm  4832  opeldmg  4834  elreldm  4855  elrn2  4871  opelresg  4916  elsnres  4946  iss  4955  elimasng  4998  issref  5013  rnxpid  5065  unielrel  5158  dffun5r  5230  funopg  5252  brprcneu  5510  tz6.12f  5546  fvelrnb  5566  ssimaex  5580  dmfco  5587  fvmpt3  5598  mptfvex  5604  fvmptf  5611  respreima  5647  fvelrn  5650  ffnfvf  5678  ffvresb  5682  fmptco  5685  fmptcof  5686  fsn  5691  fressnfv  5706  fnex  5741  funfvima  5751  funfvima3  5753  f1mpt  5775  fliftfuns  5802  isoselem  5824  ovrspc2v  5904  ffnov  5982  fovcl  5983  ovmpos  6001  ov2gf  6002  ovg  6016  funimassov  6027  caovclg  6030  elovmpo  6075  off  6098  fnexALT  6115  focdmex  6119  f1stres  6163  f2ndres  6164  xp1st  6169  xp2nd  6170  elxp6  6173  oprssdmm  6175  unielxp  6178  fmpox  6204  mpofvex  6207  opeliunxp2f  6242  dftpos4  6267  smoel  6304  tfrlem3-2d  6316  tfrlem8  6322  tfrlem9  6323  tfrlemibxssdm  6331  tfrlemi1  6336  tfrexlem  6338  tfr1onlemsucfn  6344  tfr1onlemsucaccv  6345  tfr1onlembxssdm  6347  tfr1onlembfn  6348  tfr1onlemaccex  6352  tfr1onlemres  6353  tfri1dALT  6355  tfrcllemsucfn  6357  tfrcllemsucaccv  6358  tfrcllembxssdm  6360  tfrcllembfn  6361  tfrcllemaccex  6365  tfrcllemres  6366  tfrcl  6368  rdgtfr  6378  rdgon  6390  frecabex  6402  frecabcl  6403  frecfcllem  6408  frecsuclem  6410  nnacl  6484  nnmcl  6485  nnmordi  6520  nnaordex  6532  nnm00  6534  erexb  6563  qliftfuns  6622  ixpsnval  6704  elixp2  6705  resixp  6736  mptelixpg  6737  elixpsn  6738  fundmen  6809  fopwdom  6839  xpf1o  6847  dif1en  6882  diffitest  6890  diffifi  6897  inffiexmid  6909  unfiexmid  6920  unfidisj  6924  fiintim  6931  xpfi  6932  ssfirab  6936  fnfi  6939  iunfidisj  6948  snexxph  6952  fidcenumlemr  6957  elfi2  6974  ctssdccl  7113  isnumi  7184  cc2lem  7268  cc3  7270  addnidpig  7338  indpi  7344  dfplpq2  7356  addclnq  7377  mulclnq  7378  nnnq0lem1  7448  addclnq0  7453  mulclnq0  7454  nqpnq0nq  7455  distrnq0  7461  prloc  7493  prarloclemlo  7496  prarloclem3  7499  prarloclem5  7502  genpml  7519  genpmu  7520  addnqprl  7531  addnqpru  7532  mulnqprl  7570  mulnqpru  7571  ltexprlemell  7600  ltexprlemelu  7601  ltexprlemdisj  7608  ltexprlemloc  7609  ltexprlemrl  7612  ltexprlemru  7614  ltexpri  7615  recexprlemm  7626  recexprlemdisj  7632  recexprlemloc  7633  recexprlem1ssl  7635  recexprlem1ssu  7636  recexpr  7640  addclsr  7755  mulclsr  7756  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  suplocsr  7811  pitonn  7850  peano2nnnn  7855  axaddrcl  7867  axmulrcl  7869  peano5nnnn  7894  axpre-suploclemres  7903  negreb  8225  negf1o  8342  eqord1  8443  eqord2  8444  cju  8921  peano2nn  8934  nn1m1nn  8940  nnaddcl  8942  nnmulcl  8943  nnsub  8961  nndivtr  8964  un0addcl  9212  un0mulcl  9213  elnnnn0  9222  elz  9258  nnnegz  9259  znegclb  9289  zaddcllempos  9293  zaddcllemneg  9295  zaddcl  9296  nzadd  9308  zmulcl  9309  elz2  9327  zneo  9357  nneoor  9358  zeo  9361  peano5uzti  9364  zindd  9374  uzp1  9564  uzaddcl  9589  supinfneg  9598  infsupneg  9599  supminfex  9600  ublbneg  9616  eqreznegel  9617  negm  9618  qmulz  9626  qnegcl  9639  irradd  9649  irrmul  9650  fzrev2  10088  negqmod0  10334  frec2uzuzd  10405  frecuzrdgrrn  10411  frec2uzrdg  10412  frecuzrdgrcl  10413  frecuzrdgsuc  10417  frecuzrdgrclt  10418  frecuzrdgg  10419  frecuzrdgsuctlem  10426  iseqovex  10459  seq3val  10461  seqvalcd  10462  seq3-1  10463  seqf  10464  seq3p1  10465  seqovcd  10466  seqp1cd  10469  seq3clss  10470  monoord  10479  monoord2  10480  ser3mono  10481  seq3split  10482  seq3caopr3  10484  seq3caopr2  10485  iseqf1olemjpcl  10498  iseqf1olemqpcl  10499  iseqf1olemfvp  10500  seq3f1olemqsumkj  10501  seq3f1olemqsum  10503  seq3f1oleml  10506  seq3f1o  10507  seq3homo  10513  seq3z  10514  seq3distr  10516  ser3ge0  10520  expp1  10530  expcllem  10534  expcl2lemap  10535  m1expcl2  10545  facnn  10710  fac0  10711  fac1  10712  faccl  10718  facdiv  10721  facndiv  10722  bccmpl  10737  bcn2  10747  bccl  10750  fihasheqf1oi  10770  seq3coll  10825  shftlem  10828  shftf  10842  seq3shft  10850  cjval  10857  cjth  10858  remim  10872  uzin2  10999  caubnd2  11129  negfi  11239  xrmaxltsup  11269  clim  11292  clim2  11294  climshftlemg  11313  climcn1  11319  climcn2  11320  iserex  11350  climub  11355  climserle  11356  climcau  11358  serf0  11363  sumfct  11385  sumrbdclem  11388  fsum3cvg  11389  summodclem3  11391  summodclem2a  11392  zsumdc  11395  fsumgcl  11397  fsum3  11398  fsumf1o  11401  isumss  11402  isumss2  11404  fsum3cvg2  11405  fsum3ser  11408  fsumcl2lem  11409  fsumsplitf  11419  sumpr  11424  sumtp  11425  fsumm1  11427  fsum1p  11429  isummulc2  11437  fsum2dlemstep  11445  fisumcom2  11449  fsumshftm  11456  fisum0diag2  11458  fsummulc2  11459  fsumge1  11472  fsum00  11473  fsumabs  11476  telfsumo  11477  telfsumo2  11478  fsumparts  11481  fsumrelem  11482  fsumiun  11488  binomlem  11494  isumshft  11501  isum1p  11503  isumrpcl  11505  cvgratnnlemnexp  11535  cvgratnnlemmn  11536  cvgratnnlemseq  11537  cvgratnnlemabsle  11538  cvgratnnlemfm  11540  cvgratnnlemrate  11541  cvgratnn  11542  cvgratz  11543  mertenslem2  11547  mertensabs  11548  clim2prod  11550  prodfap0  11556  prodfrecap  11557  prodfdivap  11558  prodrbdclem  11582  fproddccvg  11583  prodmodclem3  11586  prodmodclem2a  11587  zproddc  11590  fprodseq  11594  prodfct  11598  fprodf1o  11599  prodssdc  11600  fprodssdc  11601  fprodmul  11602  fprodm1  11609  fprod1p  11610  fprodm1s  11612  fprodp1s  11613  fprodcl2lem  11616  fprodabs  11627  fprod2dlemstep  11633  fprodcnv  11636  fprodcom2fi  11637  fprodrec  11640  fproddivapf  11642  fprodsplitf  11643  fprodsplit1f  11645  fprodle  11651  zeo3  11876  mulsucdiv2z  11893  zob  11899  nn0o1gt2  11913  nno  11914  nn0o  11915  infssuzex  11953  infssuzcldc  11955  zsupssdc  11958  uzwodc  12041  qnumdencl  12190  pcqcl  12309  pcxnn0cl  12313  pcxcl  12314  pcgcd1  12330  dvdsprmpweqle  12339  pcmpt  12344  pcmpt2  12345  pcmptdvds  12346  infpnlem2  12361  1arith  12368  elgz  12372  mul4sq  12395  znnen  12402  ennnfonelemj0  12405  ennnfonelemg  12407  ennnfonelemom  12412  ctinfom  12432  ctiunctlemu1st  12438  ctiunctlemu2nd  12439  ctiunctlemudc  12441  ctiunctlemfo  12443  ssnnctlemct  12450  infpn2  12460  isstruct2im  12475  isstruct2r  12476  imasaddfnlemg  12741  ercpbl  12757  xpsfrnel2  12772  mgmsscl  12787  mgm1  12796  mndpropd  12849  issubm  12871  0subm  12879  insubm  12880  mhmima  12883  mulgsubcl  13011  issubg  13047  subgex  13050  issubg2m  13063  issubg4m  13067  0subg  13073  isnsg  13076  isnsg2  13077  nsgbi  13078  isnsg3  13081  elnmz  13082  nmzbi  13083  nmzsubg  13084  nmznsg  13087  releqgg  13094  eqgex  13095  eqgval  13097  eqgid  13100  ablnsg  13145  isrng  13160  issrg  13186  srgfcl  13194  isring  13221  iscrng  13224  dvdsrd  13301  unitsubm  13326  issubrg  13380  subrgsubm  13393  subrgugrp  13399  issubrg2  13400  issubrg3  13406  subrgpropd  13407  aprval  13410  aprsym  13412  islmod  13419  lmodlema  13420  islmodd  13421  lmodprop2d  13476  rmodislmodlem  13478  rmodislmod  13479  lsssetm  13482  islssmd  13484  lssclg  13489  lsslss  13506  lsspropdg  13556  uniopn  13689  inopn  13691  fiinopn  13692  iscld  13791  iuncld  13803  tgrest  13857  iscn  13885  cnpval  13886  iscnp  13887  tgcn  13896  ssidcn  13898  lmbrf  13903  cnpnei  13907  cnima  13908  cnconst2  13921  cnrest2  13924  cnptopresti  13926  cnptoprest  13927  lmres  13936  lmtopcnp  13938  txbasval  13955  tx1cn  13957  tx2cn  13958  txcnp  13959  txcnmpt  13961  txdis1cn  13966  txlm  13967  cnmpt11  13971  cnmpt12  13975  cnmpt21  13979  cnmpt22  13982  ishmeo  13992  hmeoopn  13999  hmeocld  14000  qtopbasss  14209  fsumcncntop  14244  expcncf  14280  ivthinclemlopn  14302  ivthinclemlr  14303  ivthinclemuopn  14304  ivthinclemur  14305  ivthinclemdisj  14306  ivthinclemloc  14307  ivthinc  14309  ivthdec  14310  limccl  14316  ellimc3apf  14317  cnmptlimc  14331  limccoap  14335  2irrexpq  14582  2irrexpqap  14584  lgsval  14593  lgsval2lem  14599  lgsdir2lem4  14620  lgsdir2  14622  m1lgs  14640  mul2sq  14651  2sqlem6  14655  bdinex1g  14841  bj-intexr  14848  bj-prexg  14851  bj-uniex  14857  bj-uniexg  14858  bdunexb  14860  bj-indsuc  14868  exmidsbthrlem  14959  qdencn  14964  iswomni0  14988