Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleqtrd | GIF version |
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
eleqtrd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
eleqtrd.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
eleqtrd | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | eleqtrd.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 2 | eleq2d 2107 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) |
4 | 1, 3 | mpbid 135 | 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: eleqtrrd 2117 3eltr3d 2120 syl5eleq 2126 syl6eleq 2130 opth1 3973 0nelop 3985 tfisi 4310 ercl 6117 erth 6150 ecelqsdm 6176 phpm 6327 lincmb01cmp 8871 fzopth 8924 fzoaddel2 9049 fzosubel2 9051 fzocatel 9055 zpnn0elfzo1 9064 fzoend 9078 peano2fzor 9088 monoord2 9236 isermono 9237 |
Copyright terms: Public domain | W3C validator |