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  5045  cnvexg  5325  opabbrex  6132  offval  6310  resfunexgALT  6337  abrexexg  6347  abrexex2g  6349  opabex3d  6350  oprssdmm  6405  unfidisj  7229  residfi  7254  ssfii  7308  djuexb  7384  nqprlu  7914  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  mertenslem2  12303  exprmfct  12916  infpnlem1  13138  4sqlem13m  13182  ballotfilemfrcn0  13273  ennnfonelemg  13294  grpidvalg  13693  gzsumvalx  13709  grppropstrg  13824  releqgg  14023  eqgex  14024  prdsval  14173  prdsbaslemss  14174  aprprop  14601  issubassa  15013  0opn  15107  difopn  15209  tgrest  15270  txbasex  15358  txdis1cn  15379  cnmptid  15382  cnmptc  15383  cnmpt1st  15389  cnmpt2nd  15390  cnmpt2c  15391  hmeoima  15411  hmeocld  15413  fsumcncntop  15668  expcn  15670  plycoeid3  15858