Theorem psseq1 4038

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 3956	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3018	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3919	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3919	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2956   ⊆ wss 3899   ⊊ wpss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957  df-ss 3916  df-pss 3919

This theorem is used by:  psseq1i  4040  psseq1d  4043  psstr  4056  sspsstr  4057  brrpssg  7730  sorpssuni  7737  pssnn  9168  marypha1lem  9409  infeq5i  9621  infpss  10275  fin4i  10357  isfin2-2  10378  zornn0g  10564  ttukeylem7  10574  elnp  11053  elnpi  11054  ltprord  11096  pgpfac1lem1  20270  pgpfac1lem5  20275  pgpfac1  20276  pgpfaclem2  20278  pgpfac  20280  islbs3  21413  alexsubALTlem4  24349  wilthlem2  27378  spansncv  32237  cvbr  32866  cvcon3  32868  cvnbtwn  32870  dfon2lem3  36517  dfon2lem4  36518  dfon2lem5  36519  dfon2lem6  36520  dfon2lem7  36521  dfon2lem8  36522  dfon2  36524  findcard4  38600  lcvbr  40046  lcvnbtwn  40050  mapdcv  42685