Theorem eleq1d 2234

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12d  2236  eqeltrd  2242  eqneltrd  2261  eqneltrrd  2262  rspcimdv  2830  rspcimedv  2831  reuind  2930  sbcel2g  3065  sbccsb2g  3074  breq1  3984  breq2  3985  inex1g  4117  intexr  4128  pwexg  4158  prexg  4188  opelopabsb  4237  pofun  4289  seex  4312  uniex  4414  uniexg  4416  unexb  4419  abnexg  4423  reusv3  4437  rabxfrd  4446  onun2  4466  onsucelsucexmid  4506  ordsucunielexmid  4507  dcextest  4557  tfisi  4563  peano2  4571  seinxp  4674  opabid2  4734  opeliunxp2  4743  elrn2g  4793  opeldm  4806  opeldmg  4808  elreldm  4829  elrn2  4845  opelresg  4890  elsnres  4920  iss  4929  elimasng  4971  issref  4985  rnxpid  5037  unielrel  5130  dffun5r  5199  funopg  5221  brprcneu  5478  tz6.12f  5514  fvelrnb  5533  ssimaex  5546  dmfco  5553  fvmpt3  5564  mptfvex  5570  fvmptf  5577  respreima  5612  fvelrn  5615  ffnfvf  5643  ffvresb  5647  fmptco  5650  fmptcof  5651  fsn  5656  fressnfv  5671  fnex  5706  funfvima  5715  funfvima3  5717  f1mpt  5738  fliftfuns  5765  isoselem  5787  ffnov  5942  fovcl  5943  ovmpos  5961  ov2gf  5962  ovg  5976  funimassov  5987  caovclg  5990  elovmpo  6038  off  6061  fnexALT  6078  fornex  6080  f1stres  6124  f2ndres  6125  xp1st  6130  xp2nd  6131  elxp6  6134  oprssdmm  6136  unielxp  6139  fmpox  6165  mpofvex  6168  opeliunxp2f  6202  dftpos4  6227  smoel  6264  tfrlem3-2d  6276  tfrlem8  6282  tfrlem9  6283  tfrlemibxssdm  6291  tfrlemi1  6296  tfrexlem  6298  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemaccex  6312  tfr1onlemres  6313  tfri1dALT  6315  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemaccex  6325  tfrcllemres  6326  tfrcl  6328  rdgtfr  6338  rdgon  6350  frecabex  6362  frecabcl  6363  frecfcllem  6368  frecsuclem  6370  nnacl  6444  nnmcl  6445  nnmordi  6480  nnaordex  6491  nnm00  6493  erexb  6522  qliftfuns  6581  ixpsnval  6663  elixp2  6664  resixp  6695  mptelixpg  6696  elixpsn  6697  fundmen  6768  fopwdom  6798  xpf1o  6806  dif1en  6841  diffitest  6849  diffifi  6856  inffiexmid  6868  unfiexmid  6879  unfidisj  6883  fiintim  6890  xpfi  6891  ssfirab  6895  fnfi  6898  iunfidisj  6907  snexxph  6911  fidcenumlemr  6916  elfi2  6933  ctssdccl  7072  isnumi  7134  cc2lem  7203  cc3  7205  addnidpig  7273  indpi  7279  dfplpq2  7291  addclnq  7312  mulclnq  7313  nnnq0lem1  7383  addclnq0  7388  mulclnq0  7389  nqpnq0nq  7390  distrnq0  7396  prloc  7428  prarloclemlo  7431  prarloclem3  7434  prarloclem5  7437  genpml  7454  genpmu  7455  addnqprl  7466  addnqpru  7467  mulnqprl  7505  mulnqpru  7506  ltexprlemell  7535  ltexprlemelu  7536  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  ltexpri  7550  recexprlemm  7561  recexprlemdisj  7567  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  recexpr  7575  addclsr  7690  mulclsr  7691  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  suplocsr  7746  pitonn  7785  peano2nnnn  7790  axaddrcl  7802  axmulrcl  7804  peano5nnnn  7829  axpre-suploclemres  7838  negreb  8159  negf1o  8276  eqord1  8377  eqord2  8378  cju  8852  peano2nn  8865  nn1m1nn  8871  nnaddcl  8873  nnmulcl  8874  nnsub  8892  nndivtr  8895  un0addcl  9143  un0mulcl  9144  elnnnn0  9153  elz  9189  nnnegz  9190  znegclb  9220  zaddcllempos  9224  zaddcllemneg  9226  zaddcl  9227  nzadd  9239  zmulcl  9240  elz2  9258  zneo  9288  nneoor  9289  zeo  9292  peano5uzti  9295  zindd  9305  uzp1  9495  uzaddcl  9520  supinfneg  9529  infsupneg  9530  supminfex  9531  ublbneg  9547  eqreznegel  9548  negm  9549  qmulz  9557  qnegcl  9570  irradd  9580  irrmul  9581  fzrev2  10016  negqmod0  10262  frec2uzuzd  10333  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  iseqovex  10387  seq3val  10389  seqvalcd  10390  seq3-1  10391  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3clss  10398  monoord  10407  monoord2  10408  ser3mono  10409  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  seq3f1oleml  10434  seq3f1o  10435  seq3homo  10441  seq3z  10442  seq3distr  10444  ser3ge0  10448  expp1  10458  expcllem  10462  expcl2lemap  10463  m1expcl2  10473  facnn  10636  fac0  10637  fac1  10638  faccl  10644  facdiv  10647  facndiv  10648  bccmpl  10663  bcn2  10673  bccl  10676  focdmex  10696  fihasheqf1oi  10697  seq3coll  10751  shftlem  10754  shftf  10768  seq3shft  10776  cjval  10783  cjth  10784  remim  10798  uzin2  10925  caubnd2  11055  negfi  11165  xrmaxltsup  11195  clim  11218  clim2  11220  climshftlemg  11239  climcn1  11245  climcn2  11246  iserex  11276  climub  11281  climserle  11282  climcau  11284  serf0  11289  sumfct  11311  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  zsumdc  11321  fsumgcl  11323  fsum3  11324  fsumf1o  11327  isumss  11328  isumss2  11330  fsum3cvg2  11331  fsum3ser  11334  fsumcl2lem  11335  fsumsplitf  11345  sumpr  11350  sumtp  11351  fsumm1  11353  fsum1p  11355  isummulc2  11363  fsum2dlemstep  11371  fisumcom2  11375  fsumshftm  11382  fisum0diag2  11384  fsummulc2  11385  fsumge1  11398  fsum00  11399  fsumabs  11402  telfsumo  11403  telfsumo2  11404  fsumparts  11407  fsumrelem  11408  fsumiun  11414  binomlem  11420  isumshft  11427  isum1p  11429  isumrpcl  11431  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratnn  11468  cvgratz  11469  mertenslem2  11473  mertensabs  11474  clim2prod  11476  prodfap0  11482  prodfrecap  11483  prodfdivap  11484  prodrbdclem  11508  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  prodfct  11524  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  fprodmul  11528  fprodm1  11535  fprod1p  11536  fprodm1s  11538  fprodp1s  11539  fprodcl2lem  11542  fprodabs  11553  fprod2dlemstep  11559  fprodcnv  11562  fprodcom2fi  11563  fprodrec  11566  fproddivapf  11568  fprodsplitf  11569  fprodsplit1f  11571  fprodle  11577  zeo3  11801  mulsucdiv2z  11818  zob  11824  nn0o1gt2  11838  nno  11839  nn0o  11840  infssuzex  11878  infssuzcldc  11880  zsupssdc  11883  uzwodc  11966  qnumdencl  12115  pcqcl  12234  pcxnn0cl  12238  pcxcl  12239  pcgcd1  12255  dvdsprmpweqle  12264  pcmpt  12269  pcmpt2  12270  pcmptdvds  12271  infpnlem2  12286  1arith  12293  elgz  12297  mul4sq  12320  znnen  12327  ennnfonelemj0  12330  ennnfonelemg  12332  ennnfonelemom  12337  ctinfom  12357  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  ctiunctlemudc  12366  ctiunctlemfo  12368  ssnnctlemct  12375  infpn2  12385  isstruct2im  12400  isstruct2r  12401  uniopn  12599  inopn  12601  fiinopn  12602  iscld  12703  iuncld  12715  tgrest  12769  iscn  12797  cnpval  12798  iscnp  12799  tgcn  12808  ssidcn  12810  lmbrf  12815  cnpnei  12819  cnima  12820  cnconst2  12833  cnrest2  12836  cnptopresti  12838  cnptoprest  12839  lmres  12848  lmtopcnp  12850  txbasval  12867  tx1cn  12869  tx2cn  12870  txcnp  12871  txcnmpt  12873  txdis1cn  12878  txlm  12879  cnmpt11  12883  cnmpt12  12887  cnmpt21  12891  cnmpt22  12894  ishmeo  12904  hmeoopn  12911  hmeocld  12912  qtopbasss  13121  fsumcncntop  13156  expcncf  13192  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  ivthinc  13221  ivthdec  13222  limccl  13228  ellimc3apf  13229  cnmptlimc  13243  limccoap  13247  2irrexpq  13494  2irrexpqap  13496  lgsval  13505  lgsval2lem  13511  lgsdir2lem4  13532  lgsdir2  13534  mul2sq  13552  2sqlem6  13556  bdinex1g  13743  bj-intexr  13750  bj-prexg  13753  bj-uniex  13759  bj-uniexg  13760  bdunexb  13762  bj-indsuc  13770  exmidsbthrlem  13861  qdencn  13866  iswomni0  13890