![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrri | GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleqtrr.1 | ⊢ 𝐴 ∈ 𝐵 |
eleqtrr.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
eleqtrri | ⊢ 𝐴 ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrr.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | eleqtrr.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2193 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | eleqtri 2264 | 1 ⊢ 𝐴 ∈ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 ∈ wcel 2160 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 |
This theorem is referenced by: 3eltr4i 2271 undifexmid 4208 opi1 4247 opi2 4248 ordpwsucexmid 4584 peano1 4608 acexmidlemcase 5887 acexmidlem2 5889 0lt2o 6461 1lt2o 6462 0elixp 6750 ac6sfi 6921 ctssdccl 7135 exmidomni 7165 exmidonfinlem 7217 exmidfodomrlemr 7226 exmidfodomrlemrALT 7227 exmidaclem 7232 pw1ne3 7254 3nelsucpw1 7258 1lt2pi 7364 prarloclemarch2 7443 prarloclemlt 7517 prarloclemcalc 7526 suplocexprlemdisj 7744 suplocexprlemub 7747 pnfxr 8035 mnfxr 8039 fnpr2ob 12809 dveflem 14624 |
Copyright terms: Public domain | W3C validator |