Theorem eqeltrid 2257

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eqeltrrid  2258  csbexga  4117  otexg  4215  tpexg  4429  dmresexg  4914  f1oabexg  5454  funfvex  5513  riotaexg  5813  riotaprop  5832  fnovex  5886  ovexg  5887  fovrn  5995  fnovrn  6000  cofunexg  6088  cofunex2g  6089  abrexex2g  6099  xpexgALT  6112  mpofvex  6182  tfrex  6347  frec0g  6376  freccllem  6381  ecexg  6517  qsexg  6569  pmex  6631  elixpsn  6713  diffifi  6872  unfidisj  6899  prfidisj  6904  tpfidisj  6905  ssfirab  6911  ssfidc  6912  fnfi  6914  funrnfi  6919  iunfidisj  6923  infclti  7000  supex2g  7010  infex2g  7011  djuex  7020  ctssdccl  7088  addvalex  7806  negcl  8119  intqfrac2  10275  intfracq  10276  frec2uzzd  10356  frecuzrdgrrn  10364  iseqf1olemqpcl  10452  seq3f1olemqsum  10456  bcval5  10697  xrmaxiflemval  11213  climmpt  11263  reccn2ap  11276  zsumdc  11347  fsumzcl2  11368  fsump1i  11396  fsumabs  11428  hash2iun1dif1  11443  mertenslemi1  11498  fprodcllemf  11576  algrf  11999  algcvg  12002  algcvga  12005  algfx  12006  eucalgcvga  12012  eucalg  12013  crth  12178  phimullem  12179  eulerthlemth  12186  prmdiv  12189  pythagtriplem11  12228  pythagtriplem13  12230  pcprecl  12243  infpnlem1  12311  infpnlem2  12312  4sqlem5  12334  mul4sqlem  12345  ennnfonelemj0  12356  ennnfonelemom  12363  ressid  12479  1strbas  12517  2strbasg  12519  2stropg  12520  restid  12590  topnvalg  12591  topnidg  12592  plusffvalg  12616  plusfvalg  12617  grpidvalg  12627  ismhm  12685  0mhm  12704  grpinvfvalg  12745  grpinvval  12746  grpinvfng  12747  grpsubfvalg  12748  grpsubval  12749  topopn  12800  topcld  12903  uncld  12907  iuncld  12909  unicld  12910  tgrest  12963  restin  12970  cnco  13015  cnrest  13029  cnptoprest2  13034  lmss  13040  txbasval  13061  txcn  13069  cnmpt12f  13080  hmeoco  13110  idhmeo  13111  blres  13228  metrest  13300  qtopbasss  13315  tgqioo  13341  divcnap  13349  fsumcncntop  13350  cncfmet  13373  cdivcncfap  13381  cnrehmeocntop  13387  cnplimcim  13430  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  2sqlem8  13753  bj-snexg  13947  trilpolemcl  14069