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 3589 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 2844 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 743 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3556 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3556 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 302 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ≠ wne 2780 ⊆ wss 3540 ⊊ wpss 3541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-ne 2782 df-in 3547 df-ss 3554 df-pss 3556 |
This theorem is referenced by: psseq1i 3658 psseq1d 3661 psstr 3673 sspsstr 3674 brrpssg 6837 sorpssuni 6844 pssnn 8063 marypha1lem 8222 infeq5i 8416 infpss 8922 fin4i 9003 isfin2-2 9024 zornn0g 9210 ttukeylem7 9220 elnp 9688 elnpi 9689 ltprord 9731 pgpfac1lem1 18296 pgpfac1lem5 18301 pgpfac1 18302 pgpfaclem2 18304 pgpfac 18306 islbs3 18976 alexsubALTlem4 21664 wilthlem2 24595 spansncv 27896 cvbr 28525 cvcon3 28527 cvnbtwn 28529 dfon2lem3 30934 dfon2lem4 30935 dfon2lem5 30936 dfon2lem6 30937 dfon2lem7 30938 dfon2lem8 30939 dfon2 30941 lcvbr 33326 lcvnbtwn 33330 mapdcv 35967 |
Copyright terms: Public domain | W3C validator |