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 3967 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 3004 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 631 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3927 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3927 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ≠ wne 2941 ⊆ wss 3908 ⊊ wpss 3909 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2942 df-v 3445 df-in 3915 df-ss 3925 df-pss 3927 |
This theorem is referenced by: psseq1i 4047 psseq1d 4050 psstr 4062 sspsstr 4063 brrpssg 7652 sorpssuni 7659 pssnn 9045 pssnnOLD 9142 marypha1lem 9302 infeq5i 9505 infpss 10086 fin4i 10167 isfin2-2 10188 zornn0g 10374 ttukeylem7 10384 elnp 10856 elnpi 10857 ltprord 10899 pgpfac1lem1 19782 pgpfac1lem5 19787 pgpfac1 19788 pgpfaclem2 19790 pgpfac 19792 islbs3 20539 alexsubALTlem4 23323 wilthlem2 26340 spansncv 30393 cvbr 31022 cvcon3 31024 cvnbtwn 31026 dfon2lem3 34150 dfon2lem4 34151 dfon2lem5 34152 dfon2lem6 34153 dfon2lem7 34154 dfon2lem8 34155 dfon2 34157 lcvbr 37378 lcvnbtwn 37382 mapdcv 40018 |
Copyright terms: Public domain | W3C validator |