Theorem eqeltrrid 2293

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  dmrnssfld  4941  cnvexg  5220  opabbrex  5989  offval  6166  resfunexgALT  6193  abrexexg  6203  abrexex2g  6205  opabex3d  6206  oprssdmm  6257  unfidisj  7019  residfi  7042  ssfii  7076  djuexb  7146  nqprlu  7660  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  mertenslem2  11847  exprmfct  12460  infpnlem1  12682  4sqlem13m  12726  ennnfonelemg  12774  prdsval  13105  prdsbaslemss  13106  grpidvalg  13205  igsumvalx  13221  grppropstrg  13351  releqgg  13556  eqgex  13557  0opn  14478  difopn  14580  tgrest  14641  txbasex  14729  txdis1cn  14750  cnmptid  14753  cnmptc  14754  cnmpt1st  14760  cnmpt2nd  14761  cnmpt2c  14762  hmeoima  14782  hmeocld  14784  fsumcncntop  15039  expcn  15041  plycoeid3  15229