Theorem psseq1 4031

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934  df-ss 3907  df-pss 3910

This theorem is referenced by:  psseq1i  4033  psseq1d  4036  psstr  4048  sspsstr  4049  brrpssg  7672  sorpssuni  7679  pssnn  9096  marypha1lem  9339  infeq5i  9548  infpss  10129  fin4i  10211  isfin2-2  10232  zornn0g  10418  ttukeylem7  10428  elnp  10901  elnpi  10902  ltprord  10944  pgpfac1lem1  20042  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem2  20050  pgpfac  20052  islbs3  21145  alexsubALTlem4  24025  wilthlem2  27046  spansncv  31739  cvbr  32368  cvcon3  32370  cvnbtwn  32372  dfon2lem3  35981  dfon2lem4  35982  dfon2lem5  35983  dfon2lem6  35984  dfon2lem7  35985  dfon2lem8  35986  dfon2  35988  lcvbr  39481  lcvnbtwn  39485  mapdcv  42120  nthrucw  47332