Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeltrrid | GIF version |
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eqeltrrid.1 | ⊢ 𝐵 = 𝐴 |
eqeltrrid.2 | ⊢ (𝜑 → 𝐵 ∈ 𝐶) |
Ref | Expression |
---|---|
eqeltrrid | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrrid.1 | . . 3 ⊢ 𝐵 = 𝐴 | |
2 | 1 | eqcomi 2174 | . 2 ⊢ 𝐴 = 𝐵 |
3 | eqeltrrid.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶) | |
4 | 2, 3 | eqeltrid 2257 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 ∈ wcel 2141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 |
This theorem is referenced by: dmrnssfld 4874 cnvexg 5148 opabbrex 5897 offval 6068 resfunexgALT 6087 abrexexg 6097 abrexex2g 6099 opabex3d 6100 oprssdmm 6150 unfidisj 6899 ssfii 6951 djuexb 7021 nqprlu 7509 iccshftr 9951 iccshftl 9953 iccdil 9955 icccntr 9957 mertenslem2 11499 exprmfct 12092 infpnlem1 12311 ennnfonelemg 12358 grpidvalg 12627 0opn 12798 difopn 12902 tgrest 12963 txbasex 13051 txdis1cn 13072 cnmptid 13075 cnmptc 13076 cnmpt1st 13082 cnmpt2nd 13083 cnmpt2c 13084 hmeoima 13104 hmeocld 13106 fsumcncntop 13350 |
Copyright terms: Public domain | W3C validator |