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  7235  residfi  7260  ssfii  7313  djuexb  7390  nqprlu  7920  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  mertenslem2  12327  exprmfct  12941  infpnlem1  13166  4sqlem13m  13210  ballotfilemfrcn0  13330  ennnfonelemg  13351  grpidvalg  13751  gzsumvalx  13767  grppropstrg  13882  releqgg  14081  eqgex  14082  prdsval  14279  prdsbaslemss  14280  aprprop  14709  issubassa  15121  0opn  15249  difopn  15351  tgrest  15412  txbasex  15500  txdis1cn  15521  cnmptid  15524  cnmptc  15525  cnmpt1st  15531  cnmpt2nd  15532  cnmpt2c  15533  hmeoima  15553  hmeocld  15555  fsumcncntop  15810  expcn  15812  plycoeid3  16000