Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6eleqr | GIF version |
Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
Ref | Expression |
---|---|
syl6eleqr.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
syl6eleqr.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
syl6eleqr | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eleqr.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | syl6eleqr.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2044 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | syl6eleq 2130 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 ∈ wcel 1393 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 |
This theorem is referenced by: brelrng 4565 elabrex 5397 fliftel1 5434 ovidig 5618 unielxp 5800 2oconcl 6022 ecopqsi 6161 eroprf 6199 isnumi 6362 addclnq 6473 mulclnq 6474 recexnq 6488 ltexnqq 6506 prarloclemarch 6516 prarloclemarch2 6517 nnnq 6520 nqnq0 6539 addclnq0 6549 mulclnq0 6550 nqpnq0nq 6551 prarloclemlt 6591 prarloclemlo 6592 prarloclemcalc 6600 nqprm 6640 cauappcvgprlem2 6758 caucvgprlem2 6778 addclsr 6838 mulclsr 6839 prsrcl 6868 pitonnlem2 6923 pitore 6926 recnnre 6927 axaddcl 6940 axmulcl 6942 axcaucvglemcl 6969 axcaucvglemval 6971 axcaucvglemcau 6972 axcaucvglemres 6973 uztrn2 8490 eluz2nn 8511 peano2uzs 8527 rebtwn2z 9109 iser0 9250 climconst 9811 climshft2 9827 clim2iser 9857 clim2iser2 9858 iiserex 9859 serif0 9871 ialgr0 9883 |
Copyright terms: Public domain | W3C validator |