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  5922  offval  6093  resfunexgALT  6112  abrexexg  6122  abrexex2g  6124  opabex3d  6125  oprssdmm  6175  unfidisj  6924  ssfii  6976  djuexb  7046  nqprlu  7549  iccshftr  9997  iccshftl  9999  iccdil  10001  icccntr  10003  mertenslem2  11547  exprmfct  12141  infpnlem1  12360  ennnfonelemg  12407  grpidvalg  12799  grppropstrg  12903  releqgg  13094  eqgex  13095  0opn  13694  difopn  13796  tgrest  13857  txbasex  13945  txdis1cn  13966  cnmptid  13969  cnmptc  13970  cnmpt1st  13976  cnmpt2nd  13977  cnmpt2c  13978  hmeoima  13998  hmeocld  14000  fsumcncntop  14244