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 3968 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)) | |
2 | neeq1 3005 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))) |
4 | df-pss 3928 | . 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶)) | |
5 | df-pss 3928 | . 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ≠ wne 2942 ⊆ wss 3909 ⊊ wpss 3910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2943 df-v 3446 df-in 3916 df-ss 3926 df-pss 3928 |
This theorem is referenced by: psseq1i 4048 psseq1d 4051 psstr 4063 sspsstr 4064 brrpssg 7653 sorpssuni 7660 pssnn 9046 pssnnOLD 9143 marypha1lem 9303 infeq5i 9506 infpss 10087 fin4i 10168 isfin2-2 10189 zornn0g 10375 ttukeylem7 10385 elnp 10857 elnpi 10858 ltprord 10900 pgpfac1lem1 19782 pgpfac1lem5 19787 pgpfac1 19788 pgpfaclem2 19790 pgpfac 19792 islbs3 20539 alexsubALTlem4 23323 wilthlem2 26340 spansncv 30381 cvbr 31010 cvcon3 31012 cvnbtwn 31014 dfon2lem3 34138 dfon2lem4 34139 dfon2lem5 34140 dfon2lem6 34141 dfon2lem7 34142 dfon2lem8 34143 dfon2 34145 lcvbr 37369 lcvnbtwn 37373 mapdcv 40009 |
Copyright terms: Public domain | W3C validator |