Theorem eqeltrrid 2265

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 2181	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2264	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  dmrnssfld  4892  cnvexg  5168  opabbrex  5921  offval  6092  resfunexgALT  6111  abrexexg  6121  abrexex2g  6123  opabex3d  6124  oprssdmm  6174  unfidisj  6923  ssfii  6975  djuexb  7045  nqprlu  7548  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  mertenslem2  11546  exprmfct  12140  infpnlem1  12359  ennnfonelemg  12406  grpidvalg  12797  grppropstrg  12900  releqgg  13085  0opn  13545  difopn  13647  tgrest  13708  txbasex  13796  txdis1cn  13817  cnmptid  13820  cnmptc  13821  cnmpt1st  13827  cnmpt2nd  13828  cnmpt2c  13829  hmeoima  13849  hmeocld  13851  fsumcncntop  14095