Theorem eqeltrrid 2295

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  dmrnssfld  4960  cnvexg  5239  opabbrex  6012  offval  6189  resfunexgALT  6216  abrexexg  6226  abrexex2g  6228  opabex3d  6229  oprssdmm  6280  unfidisj  7045  residfi  7068  ssfii  7102  djuexb  7172  nqprlu  7695  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  mertenslem2  11962  exprmfct  12575  infpnlem1  12797  4sqlem13m  12841  ennnfonelemg  12889  prdsval  13220  prdsbaslemss  13221  grpidvalg  13320  igsumvalx  13336  grppropstrg  13466  releqgg  13671  eqgex  13672  0opn  14593  difopn  14695  tgrest  14756  txbasex  14844  txdis1cn  14865  cnmptid  14868  cnmptc  14869  cnmpt1st  14875  cnmpt2nd  14876  cnmpt2c  14877  hmeoima  14897  hmeocld  14899  fsumcncntop  15154  expcn  15156  plycoeid3  15344