![]() |
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 4021 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)) | |
2 | neeq2 3001 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | |
3 | 1, 2 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))) |
4 | df-pss 3982 | . 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴)) | |
5 | df-pss 3982 | . 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ≠ wne 2937 ⊆ wss 3962 ⊊ wpss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-cleq 2726 df-ne 2938 df-ss 3979 df-pss 3982 |
This theorem is referenced by: psseq2i 4102 psseq2d 4105 psssstr 4118 brrpssg 7743 sorpssint 7751 pssnn 9206 php 9244 phpOLD 9256 php2OLD 9257 isfin4 10334 fin2i2 10355 elnp 11024 elnpi 11025 ltprord 11067 pgpfac1lem1 20108 pgpfac1lem5 20113 lbsextlem4 21180 alexsubALTlem4 24073 spansncv 31681 cvbr 32310 cvcon3 32312 cvnbtwn 32314 cvbr4i 32395 ssdifidlprm 33465 ssmxidl 33481 dfon2lem6 35769 dfon2lem7 35770 dfon2lem8 35771 dfon2 35773 lcvbr 39002 lcvnbtwn 39006 lsatcv0 39012 lsat0cv 39014 islshpcv 39034 mapdcv 41642 pssn0 42244 |
Copyright terms: Public domain | W3C validator |