![]() |
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 3876 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
2 | neeq2 3023 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | |
3 | 1, 2 | anbi12d 622 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))) |
4 | df-pss 3838 | . 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴)) | |
5 | df-pss 3838 | . 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 306 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 ≠ wne 2960 ⊆ wss 3822 ⊊ wpss 3823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-ne 2961 df-in 3829 df-ss 3836 df-pss 3838 |
This theorem is referenced by: psseq2i 3950 psseq2d 3953 psssstr 3966 brrpssg 7267 sorpssint 7275 php 8495 php2 8496 pssnn 8529 isfin4 9515 fin2i2 9536 elnp 10205 elnpi 10206 ltprord 10248 pgpfac1lem1 18958 pgpfac1lem5 18963 lbsextlem4 19667 alexsubALTlem4 22377 spansncv 29226 cvbr 29855 cvcon3 29857 cvnbtwn 29859 cvbr4i 29940 dfon2lem6 32590 dfon2lem7 32591 dfon2lem8 32592 dfon2 32594 lcvbr 35639 lcvnbtwn 35643 lsatcv0 35649 lsat0cv 35651 islshpcv 35671 mapdcv 38278 pssn0 38596 |
Copyright terms: Public domain | W3C validator |