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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  dmrnssfld  5047  cnvexg  5328  opabbrex  6135  offval  6314  resfunexgALT  6341  abrexexg  6351  abrexex2g  6353  opabex3d  6354  oprssdmm  6409  unfidisj  7233  residfi  7258  ssfii  7313  djuexb  7390  nqprlu  7920  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  mertenslem2  12328  exprmfct  12942  infpnlem1  13167  4sqlem13m  13211  ballotfilemfrcn0  13331  ennnfonelemg  13352  grpidvalg  13752  gzsumvalx  13768  grppropstrg  13883  releqgg  14082  eqgex  14083  prdsval  14280  prdsbaslemss  14281  aprprop  14710  issubassa  15122  0opn  15232  difopn  15334  tgrest  15395  txbasex  15483  txdis1cn  15504  cnmptid  15507  cnmptc  15508  cnmpt1st  15514  cnmpt2nd  15515  cnmpt2c  15516  hmeoima  15536  hmeocld  15538  fsumcncntop  15793  expcn  15795  plycoeid3  15983