Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqsstrd | GIF version |
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
eqsstrd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqsstrd.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
eqsstrd | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstrd.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
2 | eqsstrd.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 2 | sseq1d 3096 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
4 | 1, 3 | mpbird 166 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 ⊆ wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: eqsstrrd 3104 eqsstrdi 3119 tfisi 4471 funresdfunsnss 5591 suppssof1 5967 phplem4dom 6724 fival 6826 fiuni 6834 cardonle 7011 exmidfodomrlemim 7025 frecuzrdgtclt 10162 ennnfonelemkh 11852 ennnfonelemf1 11858 strfvssn 11908 setscom 11926 tgrest 12265 resttopon 12267 rest0 12275 lmtopcnp 12346 metequiv2 12592 xmettx 12606 ellimc3apf 12725 dvfvalap 12746 dvcjbr 12768 dvcj 12769 dvfre 12770 nnsf 13126 |
Copyright terms: Public domain | W3C validator |