Theorem psseq1 4030

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 3947	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2994	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3909	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3909	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ≠ wne 2932   ⊆ wss 3889   ⊊ wpss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933  df-ss 3906  df-pss 3909

This theorem is referenced by:  psseq1i  4032  psseq1d  4035  psstr  4047  sspsstr  4048  brrpssg  7679  sorpssuni  7686  pssnn  9103  marypha1lem  9346  infeq5i  9557  infpss  10138  fin4i  10220  isfin2-2  10241  zornn0g  10427  ttukeylem7  10437  elnp  10910  elnpi  10911  ltprord  10953  pgpfac1lem1  20051  pgpfac1lem5  20056  pgpfac1  20057  pgpfaclem2  20059  pgpfac  20061  islbs3  21153  alexsubALTlem4  24015  wilthlem2  27032  spansncv  31724  cvbr  32353  cvcon3  32355  cvnbtwn  32357  dfon2lem3  35965  dfon2lem4  35966  dfon2lem5  35967  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  lcvbr  39467  lcvnbtwn  39471  mapdcv  42106  nthrucw  47316