![]() |
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 2099 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | eleqtri 2169 | 1 ⊢ 𝐴 ∈ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1296 ∈ wcel 1445 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-cleq 2088 df-clel 2091 |
This theorem is referenced by: 3eltr4i 2176 undifexmid 4049 opi1 4083 opi2 4084 ordpwsucexmid 4414 peano1 4437 acexmidlemcase 5685 acexmidlem2 5687 0lt2o 6243 1lt2o 6244 0elixp 6526 ac6sfi 6694 djuun 6840 exmidomni 6885 infnninf 6893 nnnninf 6894 exmidfodomrlemr 6925 exmidfodomrlemrALT 6926 1lt2pi 6996 prarloclemarch2 7075 prarloclemlt 7149 prarloclemcalc 7158 pnfxr 7637 mnfxr 7641 |
Copyright terms: Public domain | W3C validator |