![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > psseq2 | Structured version Visualization version GIF version |
Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.) |
Ref | Expression |
---|---|
psseq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3776 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
2 | neeq2 3006 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | |
3 | 1, 2 | anbi12d 616 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))) |
4 | df-pss 3739 | . 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴)) | |
5 | df-pss 3739 | . 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ≠ wne 2943 ⊆ wss 3723 ⊊ wpss 3724 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-ne 2944 df-in 3730 df-ss 3737 df-pss 3739 |
This theorem is referenced by: psseq2i 3847 psseq2d 3850 psssstr 3863 brrpssg 7086 sorpssint 7094 php 8300 php2 8301 pssnn 8334 isfin4 9321 fin2i2 9342 elnp 10011 elnpi 10012 ltprord 10054 pgpfac1lem1 18681 pgpfac1lem5 18686 lbsextlem4 19376 alexsubALTlem4 22074 spansncv 28852 cvbr 29481 cvcon3 29483 cvnbtwn 29485 cvbr4i 29566 dfon2lem6 32029 dfon2lem7 32030 dfon2lem8 32031 dfon2 32033 lcvbr 34830 lcvnbtwn 34834 lsatcv0 34840 lsat0cv 34842 islshpcv 34862 mapdcv 37470 pssn0 37775 |
Copyright terms: Public domain | W3C validator |