Theorem eqeltrid 2264

Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrid.1	⊢ 𝐴 = 𝐵
eqeltrid.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrd 2254	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = 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:  eqeltrrid  2265  csbexga  4131  otexg  4230  tpexg  4444  dmresexg  4930  f1oabexg  5473  funfvex  5532  riotaexg  5834  riotaprop  5853  fnovex  5907  ovexg  5908  fovcdm  6016  fnovrn  6021  cofunexg  6109  cofunex2g  6110  abrexex2g  6120  xpexgALT  6133  mpofvex  6203  tfrex  6368  frec0g  6397  freccllem  6402  ecexg  6538  qsexg  6590  pmex  6652  elixpsn  6734  diffifi  6893  unfidisj  6920  prfidisj  6925  tpfidisj  6926  ssfirab  6932  ssfidc  6933  fnfi  6935  funrnfi  6940  iunfidisj  6944  infclti  7021  supex2g  7031  infex2g  7032  djuex  7041  ctssdccl  7109  addvalex  7842  negcl  8155  intqfrac2  10316  intfracq  10317  frec2uzzd  10397  frecuzrdgrrn  10405  iseqf1olemqpcl  10493  seq3f1olemqsum  10497  bcval5  10738  xrmaxiflemval  11253  climmpt  11303  reccn2ap  11316  zsumdc  11387  fsumzcl2  11408  fsump1i  11436  fsumabs  11468  hash2iun1dif1  11483  mertenslemi1  11538  fprodcllemf  11616  algrf  12039  algcvg  12042  algcvga  12045  algfx  12046  eucalgcvga  12052  eucalg  12053  crth  12218  phimullem  12219  eulerthlemth  12226  prmdiv  12229  pythagtriplem11  12268  pythagtriplem13  12270  pcprecl  12283  infpnlem1  12351  infpnlem2  12352  4sqlem5  12374  mul4sqlem  12385  ennnfonelemj0  12396  ennnfonelemom  12403  ressval3d  12525  1strbas  12570  2strbasg  12572  2stropg  12573  restid  12689  topnvalg  12690  topnidg  12691  imasival  12709  imasmulr  12712  imasaddfn  12720  imasaddval  12721  imasaddf  12722  imasmulfn  12723  imasmulval  12724  imasmulf  12725  plusffvalg  12735  plusfvalg  12736  grpidvalg  12746  issubmnd  12797  ress0g  12798  ismhm  12807  0mhm  12827  grpinvfvalg  12869  grpinvval  12870  grpinvfng  12871  grpsubfvalg  12872  grpsubval  12873  grpressid  12885  grplactfval  12925  mulgfvalg  12939  mulgval  12940  mulgfng  12941  mulgnnp1  12945  mulgnndir  12965  issubg  12986  subggrp  12990  issubg2m  13002  eqgfval  13034  eqgen  13039  mgpvalg  13086  mgpplusgg  13087  mgptopng  13092  mgpress  13094  issrg  13101  ringidss  13165  ring1  13189  ringressid  13191  opprvalg  13194  opprmulfvalg  13195  rdivmuldivd  13266  issubrg  13302  subrgring  13305  topopn  13399  topcld  13502  uncld  13506  iuncld  13508  unicld  13509  tgrest  13562  restin  13569  cnco  13614  cnrest  13628  cnptoprest2  13633  lmss  13639  txbasval  13660  txcn  13668  cnmpt12f  13679  hmeoco  13709  idhmeo  13710  blres  13827  metrest  13899  qtopbasss  13914  tgqioo  13940  divcnap  13948  fsumcncntop  13949  cncfmet  13972  cdivcncfap  13980  cnrehmeocntop  13986  cnplimcim  14029  limccnpcntop  14037  limccnp2lem  14038  limccnp2cntop  14039  dvfvalap  14043  2sqlem8  14352  bj-snexg  14546  trilpolemcl  14667