Theorem psseq1 4037

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
psseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Proof of Theorem psseq1

Step	Hyp	Ref	Expression
1		sseq1 3955	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2990	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3917	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3917	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2928   ⊆ wss 3897   ⊊ wpss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929  df-ss 3914  df-pss 3917

This theorem is referenced by:  psseq1i  4039  psseq1d  4042  psstr  4054  sspsstr  4055  brrpssg  7658  sorpssuni  7665  pssnn  9078  marypha1lem  9317  infeq5i  9526  infpss  10107  fin4i  10189  isfin2-2  10210  zornn0g  10396  ttukeylem7  10406  elnp  10878  elnpi  10879  ltprord  10921  pgpfac1lem1  19988  pgpfac1lem5  19993  pgpfac1  19994  pgpfaclem2  19996  pgpfac  19998  islbs3  21092  alexsubALTlem4  23965  wilthlem2  27006  spansncv  31633  cvbr  32262  cvcon3  32264  cvnbtwn  32266  dfon2lem3  35827  dfon2lem4  35828  dfon2lem5  35829  dfon2lem6  35830  dfon2lem7  35831  dfon2lem8  35832  dfon2  35834  lcvbr  39119  lcvnbtwn  39123  mapdcv  41758  nthrucw  46983