![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > psseq1 | Structured version Visualization version GIF version |
Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
psseq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq1 4020 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 3000 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3982 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3982 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ≠ wne 2937 ⊆ wss 3962 ⊊ wpss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-cleq 2726 df-ne 2938 df-ss 3979 df-pss 3982 |
This theorem is referenced by: psseq1i 4101 psseq1d 4104 psstr 4116 sspsstr 4117 brrpssg 7743 sorpssuni 7750 pssnn 9206 marypha1lem 9470 infeq5i 9673 infpss 10253 fin4i 10335 isfin2-2 10356 zornn0g 10542 ttukeylem7 10552 elnp 11024 elnpi 11025 ltprord 11067 pgpfac1lem1 20108 pgpfac1lem5 20113 pgpfac1 20114 pgpfaclem2 20116 pgpfac 20118 islbs3 21174 alexsubALTlem4 24073 wilthlem2 27126 spansncv 31681 cvbr 32310 cvcon3 32312 cvnbtwn 32314 dfon2lem3 35766 dfon2lem4 35767 dfon2lem5 35768 dfon2lem6 35769 dfon2lem7 35770 dfon2lem8 35771 dfon2 35773 lcvbr 39002 lcvnbtwn 39006 mapdcv 41642 |
Copyright terms: Public domain | W3C validator |