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 2240 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) |
4 | 1, 3 | mpbid 146 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 ∈ wcel 2141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 |
This theorem is referenced by: eleqtrrd 2250 3eltr3d 2253 eleqtrid 2259 eleqtrdi 2263 opth1 4219 0nelop 4231 tfisi 4569 nnpredlt 4606 iotam 5188 ercl 6522 erth 6555 ecelqsdm 6581 phpm 6841 exmidpweq 6885 cc2lem 7221 cc3 7223 suplocexprlemmu 7673 suplocexprlemloc 7676 lincmb01cmp 9953 fzopth 10010 fzoaddel2 10142 fzosubel2 10144 fzocatel 10148 zpnn0elfzo1 10157 fzoend 10171 peano2fzor 10181 monoord2 10426 ser3mono 10427 bcpasc 10693 zfz1isolemiso 10767 fisum0diag2 11403 isumsplit 11447 prodmodclem3 11531 prodmodclem2a 11532 nnmindc 11982 nnminle 11983 basmexd 12468 mgm1 12617 grpidd 12630 ismndd 12666 mndpropd 12669 grpidd2 12737 iscnp4 12977 cnrest2r 12996 txbasval 13026 txlm 13038 xmetunirn 13117 xblss2ps 13163 blbas 13192 mopntopon 13202 isxms2 13211 metcnpi 13274 metcnpi2 13275 tgioo 13305 cncfmpt2fcntop 13344 limccl 13387 limcimolemlt 13392 limccnp2cntop 13405 dvmulxxbr 13425 dvcoapbr 13430 dvcjbr 13431 dvrecap 13436 |
Copyright terms: Public domain | W3C validator |