Theorem eqeltrid 2252

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

Syntax hints:   → wi 4   = 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:  eqeltrrid  2253  csbexga  4109  otexg  4207  tpexg  4421  dmresexg  4906  f1oabexg  5443  funfvex  5502  riotaexg  5801  riotaprop  5820  fnovex  5871  ovexg  5872  fovrn  5980  fnovrn  5985  cofunexg  6076  cofunex2g  6077  abrexex2g  6085  xpexgALT  6098  mpofvex  6168  tfrex  6332  frec0g  6361  freccllem  6366  ecexg  6501  qsexg  6553  pmex  6615  elixpsn  6697  diffifi  6856  unfidisj  6883  prfidisj  6888  tpfidisj  6889  ssfirab  6895  ssfidc  6896  fnfi  6898  funrnfi  6903  iunfidisj  6907  infclti  6984  supex2g  6994  infex2g  6995  djuex  7004  ctssdccl  7072  addvalex  7781  negcl  8094  intqfrac2  10250  intfracq  10251  frec2uzzd  10331  frecuzrdgrrn  10339  iseqf1olemqpcl  10427  seq3f1olemqsum  10431  bcval5  10672  xrmaxiflemval  11187  climmpt  11237  reccn2ap  11250  zsumdc  11321  fsumzcl2  11342  fsump1i  11370  fsumabs  11402  hash2iun1dif1  11417  mertenslemi1  11472  fprodcllemf  11550  algrf  11973  algcvg  11976  algcvga  11979  algfx  11980  eucalgcvga  11986  eucalg  11987  crth  12152  phimullem  12153  eulerthlemth  12160  prmdiv  12163  pythagtriplem11  12202  pythagtriplem13  12204  pcprecl  12217  infpnlem1  12285  infpnlem2  12286  4sqlem5  12308  mul4sqlem  12319  ennnfonelemj0  12330  ennnfonelemom  12337  ressid  12451  1strbas  12489  2strbasg  12491  2stropg  12492  restid  12562  topnvalg  12563  topnidg  12564  topopn  12606  topcld  12709  uncld  12713  iuncld  12715  unicld  12716  tgrest  12769  restin  12776  cnco  12821  cnrest  12835  cnptoprest2  12840  lmss  12846  txbasval  12867  txcn  12875  cnmpt12f  12886  hmeoco  12916  idhmeo  12917  blres  13034  metrest  13106  qtopbasss  13121  tgqioo  13147  divcnap  13155  fsumcncntop  13156  cncfmet  13179  cdivcncfap  13187  cnrehmeocntop  13193  cnplimcim  13236  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  dvfvalap  13250  2sqlem8  13559  bj-snexg  13754  trilpolemcl  13876