Theorem psseq1 4056

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2926   ⊆ wss 3917   ⊊ wpss 3918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927  df-ss 3934  df-pss 3937

This theorem is referenced by:  psseq1i  4058  psseq1d  4061  psstr  4073  sspsstr  4074  brrpssg  7704  sorpssuni  7711  pssnn  9138  marypha1lem  9391  infeq5i  9596  infpss  10176  fin4i  10258  isfin2-2  10279  zornn0g  10465  ttukeylem7  10475  elnp  10947  elnpi  10948  ltprord  10990  pgpfac1lem1  20013  pgpfac1lem5  20018  pgpfac1  20019  pgpfaclem2  20021  pgpfac  20023  islbs3  21072  alexsubALTlem4  23944  wilthlem2  26986  spansncv  31589  cvbr  32218  cvcon3  32220  cvnbtwn  32222  dfon2lem3  35780  dfon2lem4  35781  dfon2lem5  35782  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon2  35787  lcvbr  39021  lcvnbtwn  39025  mapdcv  41661