Theorem eqeltrid 2227

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

Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eqeltrrid  2228  csbexga  4064  otexg  4160  tpexg  4373  dmresexg  4850  f1oabexg  5387  funfvex  5446  riotaexg  5742  riotaprop  5761  fnovex  5812  ovexg  5813  fovrn  5921  fnovrn  5926  cofunexg  6017  cofunex2g  6018  abrexex2g  6026  xpexgALT  6039  mpofvex  6109  tfrex  6273  frec0g  6302  freccllem  6307  ecexg  6441  qsexg  6493  pmex  6555  elixpsn  6637  diffifi  6796  unfidisj  6818  prfidisj  6823  tpfidisj  6824  ssfirab  6830  ssfidc  6831  fnfi  6833  funrnfi  6838  iunfidisj  6842  infclti  6918  djuex  6936  ctssdccl  7004  addvalex  7676  negcl  7986  intqfrac2  10123  intfracq  10124  frec2uzzd  10204  frecuzrdgrrn  10212  iseqf1olemqpcl  10300  seq3f1olemqsum  10304  bcval5  10541  xrmaxiflemval  11051  climmpt  11101  reccn2ap  11114  zsumdc  11185  fsumzcl2  11206  fsump1i  11234  fsumabs  11266  hash2iun1dif1  11281  mertenslemi1  11336  algrf  11762  algcvg  11765  algcvga  11768  algfx  11769  eucalgcvga  11775  eucalg  11776  crth  11936  phimullem  11937  ennnfonelemj0  11950  ennnfonelemom  11957  ressid  12059  1strbas  12097  2strbasg  12099  2stropg  12100  restid  12170  topnvalg  12171  topnidg  12172  topopn  12214  topcld  12317  uncld  12321  iuncld  12323  unicld  12324  tgrest  12377  restin  12384  cnco  12429  cnrest  12443  cnptoprest2  12448  lmss  12454  txbasval  12475  txcn  12483  cnmpt12f  12494  hmeoco  12524  idhmeo  12525  blres  12642  metrest  12714  qtopbasss  12729  tgqioo  12755  divcnap  12763  fsumcncntop  12764  cncfmet  12787  cdivcncfap  12795  cnrehmeocntop  12801  cnplimcim  12844  limccnpcntop  12852  limccnp2lem  12853  limccnp2cntop  12854  dvfvalap  12858  bj-snexg  13281  trilpolemcl  13405