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 3991 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 3078 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3953 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3953 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 315 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ≠ wne 3016 ⊆ wss 3935 ⊊ wpss 3936 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ne 3017 df-in 3942 df-ss 3951 df-pss 3953 |
This theorem is referenced by: psseq1i 4065 psseq1d 4068 psstr 4080 sspsstr 4081 brrpssg 7440 sorpssuni 7447 pssnn 8725 marypha1lem 8886 infeq5i 9088 infpss 9628 fin4i 9709 isfin2-2 9730 zornn0g 9916 ttukeylem7 9926 elnp 10398 elnpi 10399 ltprord 10441 pgpfac1lem1 19127 pgpfac1lem5 19132 pgpfac1 19133 pgpfaclem2 19135 pgpfac 19137 islbs3 19858 alexsubALTlem4 22588 wilthlem2 25574 spansncv 29358 cvbr 29987 cvcon3 29989 cvnbtwn 29991 dfon2lem3 32928 dfon2lem4 32929 dfon2lem5 32930 dfon2lem6 32931 dfon2lem7 32932 dfon2lem8 32933 dfon2 32935 lcvbr 36039 lcvnbtwn 36043 mapdcv 38678 |
Copyright terms: Public domain | W3C validator |