Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseq12d | GIF version |
Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.) |
Ref | Expression |
---|---|
sseq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
sseq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
sseq12d | ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | sseq1d 3121 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) |
3 | sseq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | sseq2d 3122 | . 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) |
5 | 2, 4 | bitrd 187 | 1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1331 ⊆ wss 3066 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-in 3072 df-ss 3079 |
This theorem is referenced by: 3sstr3d 3136 3sstr4d 3137 ssdifeq0 3440 relcnvtr 5053 rdgisucinc 6275 oawordriexmid 6359 nnaword 6400 nnawordi 6404 sbthlem2 6839 isbth 6848 infnninf 7015 nnnninf 7016 ennnfonelemkh 11914 ennnfonelemrnh 11918 isstruct2im 11958 isstruct2r 11959 ressid2 12007 ressval2 12008 basis1 12203 baspartn 12206 eltg 12210 metss 12652 0nninf 13186 nninff 13187 nnsf 13188 peano4nninf 13189 nninfalllemn 13191 nninfalllem1 13192 nninfself 13198 |
Copyright terms: Public domain | W3C validator |