![]() |
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 3659 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 2885 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 747 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3623 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3623 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ≠ wne 2823 ⊆ wss 3607 ⊊ wpss 3608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-ne 2824 df-in 3614 df-ss 3621 df-pss 3623 |
This theorem is referenced by: psseq1i 3729 psseq1d 3732 psstr 3744 sspsstr 3745 brrpssg 6981 sorpssuni 6988 pssnn 8219 marypha1lem 8380 infeq5i 8571 infpss 9077 fin4i 9158 isfin2-2 9179 zornn0g 9365 ttukeylem7 9375 elnp 9847 elnpi 9848 ltprord 9890 pgpfac1lem1 18519 pgpfac1lem5 18524 pgpfac1 18525 pgpfaclem2 18527 pgpfac 18529 islbs3 19203 alexsubALTlem4 21901 wilthlem2 24840 spansncv 28640 cvbr 29269 cvcon3 29271 cvnbtwn 29273 dfon2lem3 31814 dfon2lem4 31815 dfon2lem5 31816 dfon2lem6 31817 dfon2lem7 31818 dfon2lem8 31819 dfon2 31821 lcvbr 34626 lcvnbtwn 34630 mapdcv 37266 |
Copyright terms: Public domain | W3C validator |