![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrrd | GIF version |
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
eleqtrrd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
eleqtrrd.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
Ref | Expression |
---|---|
eleqtrrd | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrrd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | eleqtrrd.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
3 | 2 | eqcomd 2146 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | eleqtrd 2219 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1332 ∈ wcel 1481 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: 3eltr4d 2224 exmidsssnc 4134 tfrexlem 6239 nnsucuniel 6399 erref 6457 en1uniel 6706 fin0 6787 fin0or 6788 prarloclemarch2 7251 fzopth 9872 fzoss2 9980 fzosubel3 10004 elfzomin 10014 elfzonlteqm1 10018 fzoend 10030 fzofzp1 10035 fzofzp1b 10036 peano2fzor 10040 zmodfzo 10151 frecuzrdg0 10217 frecuzrdgsuc 10218 frecuzrdgdomlem 10221 frecuzrdg0t 10226 frecuzrdgsuctlem 10227 seq3f1olemqsum 10304 bcn2 10542 summodclem2a 11182 fisumss 11193 fsumm1 11217 fisumcom2 11239 prodmodclem2a 11377 ennnfonelemex 11963 ctinfomlemom 11976 lmtopcnp 12458 txopn 12473 blpnfctr 12647 metcnpi 12723 metcnpi2 12724 cncfmpt2fcntop 12793 limcimolemlt 12841 cnplimclemr 12846 limccnp2lem 12853 limccnp2cntop 12854 dvidlemap 12868 dvcnp2cntop 12871 dvcn 12872 dvaddxxbr 12873 dvmulxxbr 12874 dvef 12896 |
Copyright terms: Public domain | W3C validator |