![]() |
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 2087 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | syl6eleq 2175 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∈ wcel 1434 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 df-clel 2079 |
This theorem is referenced by: brelrng 4624 elabrex 5477 fliftel1 5513 ovidig 5697 unielxp 5879 2oconcl 6135 ecopqsi 6277 eroprf 6315 djulclr 6648 djurclr 6649 djulcl 6650 djurcl 6651 isnumi 6713 addclnq 6837 mulclnq 6838 recexnq 6852 ltexnqq 6870 prarloclemarch 6880 prarloclemarch2 6881 nnnq 6884 nqnq0 6903 addclnq0 6913 mulclnq0 6914 nqpnq0nq 6915 prarloclemlt 6955 prarloclemlo 6956 prarloclemcalc 6964 nqprm 7004 cauappcvgprlem2 7122 caucvgprlem2 7142 addclsr 7202 mulclsr 7203 prsrcl 7232 pitonnlem2 7287 pitore 7290 recnnre 7291 axaddcl 7304 axmulcl 7306 axcaucvglemcl 7333 axcaucvglemval 7335 axcaucvglemcau 7336 axcaucvglemres 7337 uztrn2 8931 eluz2nn 8952 peano2uzs 8967 rebtwn2z 9555 iseqfcl 9754 iseqfclt 9755 iser0 9787 bcm1k 10003 bcp1nk 10005 bcpasc 10009 hashennn 10023 hashcl 10024 climconst 10503 climshft2 10519 clim2iser 10549 clim2iser2 10550 iiserex 10551 serif0 10563 dvdsflip 10632 fzo0dvdseq 10638 gcdsupcl 10730 ialgr0 10806 prmind2 10882 crth 10980 djulclALT 11044 djurclALT 11045 |
Copyright terms: Public domain | W3C validator |