Theorem psseq1 4040

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

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

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 3919  df-pss 3922

This theorem is referenced by:  psseq1i  4042  psseq1d  4045  psstr  4057  sspsstr  4058  brrpssg  7658  sorpssuni  7665  pssnn  9078  marypha1lem  9317  infeq5i  9526  infpss  10104  fin4i  10186  isfin2-2  10207  zornn0g  10393  ttukeylem7  10403  elnp  10875  elnpi  10876  ltprord  10918  pgpfac1lem1  19986  pgpfac1lem5  19991  pgpfac1  19992  pgpfaclem2  19994  pgpfac  19996  islbs3  21090  alexsubALTlem4  23963  wilthlem2  27004  spansncv  31628  cvbr  32257  cvcon3  32259  cvnbtwn  32261  dfon2lem3  35818  dfon2lem4  35819  dfon2lem5  35820  dfon2lem6  35821  dfon2lem7  35822  dfon2lem8  35823  dfon2  35825  lcvbr  39059  lcvnbtwn  39063  mapdcv  41698