Theorem eqeltrrid 2317

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  dmrnssfld  4986  cnvexg  5265  opabbrex  6047  offval  6224  resfunexgALT  6251  abrexexg  6261  abrexex2g  6263  opabex3d  6264  oprssdmm  6315  unfidisj  7080  residfi  7103  ssfii  7137  djuexb  7207  nqprlu  7730  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  mertenslem2  12042  exprmfct  12655  infpnlem1  12877  4sqlem13m  12921  ennnfonelemg  12969  prdsval  13301  prdsbaslemss  13302  grpidvalg  13401  igsumvalx  13417  grppropstrg  13547  releqgg  13752  eqgex  13753  0opn  14674  difopn  14776  tgrest  14837  txbasex  14925  txdis1cn  14946  cnmptid  14949  cnmptc  14950  cnmpt1st  14956  cnmpt2nd  14957  cnmpt2c  14958  hmeoima  14978  hmeocld  14980  fsumcncntop  15235  expcn  15237  plycoeid3  15425