Theorem eqeltrrid 2326

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2242	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2325	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  dmrnssfld  5040  cnvexg  5320  opabbrex  6122  offval  6300  resfunexgALT  6327  abrexexg  6337  abrexex2g  6339  opabex3d  6340  oprssdmm  6395  unfidisj  7219  residfi  7244  ssfii  7298  djuexb  7374  nqprlu  7904  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  mertenslem2  12281  exprmfct  12894  infpnlem1  13116  4sqlem13m  13160  ballotfilemfrcn0  13251  ennnfonelemg  13272  grpidvalg  13670  gzsumvalx  13686  grppropstrg  13801  releqgg  14000  eqgex  14001  prdsval  14150  prdsbaslemss  14151  aprprop  14574  0opn  15030  difopn  15132  tgrest  15193  txbasex  15281  txdis1cn  15302  cnmptid  15305  cnmptc  15306  cnmpt1st  15312  cnmpt2nd  15313  cnmpt2c  15314  hmeoima  15334  hmeocld  15336  fsumcncntop  15591  expcn  15593  plycoeid3  15781