Theorem psseq1 4053

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3914   ⊊ wpss 3915

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926  df-ss 3931  df-pss 3934

This theorem is referenced by:  psseq1i  4055  psseq1d  4058  psstr  4070  sspsstr  4071  brrpssg  7701  sorpssuni  7708  pssnn  9132  marypha1lem  9384  infeq5i  9589  infpss  10169  fin4i  10251  isfin2-2  10272  zornn0g  10458  ttukeylem7  10468  elnp  10940  elnpi  10941  ltprord  10983  pgpfac1lem1  20006  pgpfac1lem5  20011  pgpfac1  20012  pgpfaclem2  20014  pgpfac  20016  islbs3  21065  alexsubALTlem4  23937  wilthlem2  26979  spansncv  31582  cvbr  32211  cvcon3  32213  cvnbtwn  32215  dfon2lem3  35773  dfon2lem4  35774  dfon2lem5  35775  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon2  35780  lcvbr  39014  lcvnbtwn  39018  mapdcv  41654