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 3996 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
2 | neeq2 3082 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))) |
4 | df-pss 3957 | . 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴)) | |
5 | df-pss 3957 | . 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ≠ wne 3019 ⊆ wss 3939 ⊊ wpss 3940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-ne 3020 df-in 3946 df-ss 3955 df-pss 3957 |
This theorem is referenced by: psseq2i 4070 psseq2d 4073 psssstr 4086 brrpssg 7454 sorpssint 7462 php 8704 php2 8705 pssnn 8739 isfin4 9722 fin2i2 9743 elnp 10412 elnpi 10413 ltprord 10455 pgpfac1lem1 19199 pgpfac1lem5 19204 lbsextlem4 19936 alexsubALTlem4 22661 spansncv 29433 cvbr 30062 cvcon3 30064 cvnbtwn 30066 cvbr4i 30147 ssmxidl 30983 dfon2lem6 33037 dfon2lem7 33038 dfon2lem8 33039 dfon2 33041 lcvbr 36161 lcvnbtwn 36165 lsatcv0 36171 lsat0cv 36173 islshpcv 36193 mapdcv 38800 pssn0 39119 |
Copyright terms: Public domain | W3C validator |