| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 3eltr4d | GIF version | ||
| Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
| Ref | Expression |
|---|---|
| 3eltr4d.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 3eltr4d.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
| 3eltr4d.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
| Ref | Expression |
|---|---|
| 3eltr4d | ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3eltr4d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐴) | |
| 2 | 3eltr4d.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
| 3 | 3eltr4d.3 | . . 3 ⊢ (𝜑 → 𝐷 = 𝐵) | |
| 4 | 2, 3 | eleqtrrd 2311 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷) |
| 5 | 1, 4 | eqeltrd 2308 | 1 ⊢ (𝜑 → 𝐶 ∈ 𝐷) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1397 ∈ wcel 2202 |
| 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 1495 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-4 1558 ax-17 1574 ax-ial 1582 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-cleq 2224 df-clel 2227 |
| This theorem is referenced by: ovmpodxf 6147 nnaordi 6676 iccf1o 10239 ccatw2s1p1g 11226 nnmindc 12610 ennnfonelemrn 13045 ctiunctlemfo 13065 sgrppropd 13501 mndpropd 13528 issubmnd 13530 imasgrp 13703 mulgnndir 13743 subg0cl 13774 subginvcl 13775 subgcl 13776 rngcl 13963 rngpropd 13974 srgcl 13989 srgidcl 13995 ringidcl 14039 ringpropd 14057 dvdsrd 14114 dvrvald 14154 subrngmcl 14229 subrgmcl 14253 subrgunit 14259 lmodprop2d 14368 lidl0 14509 lidl1 14510 psraddcl 14700 wlkl1loop 16215 wlkres 16236 clwwlknonex2lem1 16294 |
| Copyright terms: Public domain | W3C validator |