![]() |
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 2259 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)) |
4 | 1, 3 | mpbid 147 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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: eleqtrrd 2269 3eltr3d 2272 eleqtrid 2278 eleqtrdi 2282 opth1 4254 0nelop 4266 tfisi 4604 nnpredlt 4641 iotam 5227 ercl 6570 erth 6605 ecelqsdm 6631 phpm 6893 exmidpweq 6937 cc2lem 7295 cc3 7297 suplocexprlemmu 7747 suplocexprlemloc 7750 lincmb01cmp 10033 fzopth 10091 fzoaddel2 10223 fzosubel2 10225 fzocatel 10229 zpnn0elfzo1 10238 fzoend 10252 peano2fzor 10262 monoord2 10508 ser3mono 10509 bcpasc 10778 zfz1isolemiso 10851 fisum0diag2 11487 isumsplit 11531 prodmodclem3 11615 prodmodclem2a 11616 nnmindc 12067 nnminle 12068 basmexd 12572 basm 12573 mgm1 12846 grpidd 12859 sgrppropd 12876 ismndd 12898 mndpropd 12901 issubmnd 12903 grpidd2 12985 imasgrp 13053 subginvcl 13122 subgcl 13123 subgsub 13125 subgmulg 13127 1nsgtrivd 13158 quseccl0g 13170 kerf1ghm 13213 rngass 13293 rngcl 13298 rngpropd 13309 imasrng 13310 srgcl 13324 srgass 13325 srg1zr 13341 srgpcomp 13344 srgpcompp 13345 srgpcomppsc 13346 crngcom 13368 ringass 13370 ringidmlem 13376 ringidss 13383 ringpropd 13392 imasring 13414 qusring2 13416 mulgass3 13435 dvdsrd 13444 1unit 13457 unitmulcl 13463 dvrvald 13484 rdivmuldivd 13494 elrhmunit 13527 rhmunitinv 13528 lringuplu 13543 subrngmcl 13556 subrg1 13578 subrgmcl 13580 subrgdv 13585 subrgunit 13586 aprval 13598 aprirr 13599 aprsym 13600 aprcotr 13601 lmodprop2d 13664 lidlss 13792 lidl0cl 13799 lidlacl 13800 lidlnegcl 13801 rnglidlmsgrp 13813 2idllidld 13821 2idlridld 13822 2idlcpblrng 13838 qus1 13841 quscrng 13847 psrelbas 13952 iscnp4 14175 cnrest2r 14194 txbasval 14224 txlm 14236 xmetunirn 14315 xblss2ps 14361 blbas 14390 mopntopon 14400 isxms2 14409 metcnpi 14472 metcnpi2 14473 tgioo 14503 cncfmpt2fcntop 14542 limccl 14585 limcimolemlt 14590 limccnp2cntop 14603 dvmulxxbr 14623 dvcoapbr 14628 dvcjbr 14629 dvrecap 14634 |
Copyright terms: Public domain | W3C validator |