Theorem psseq1 4017

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ≠ wne 2955   ⊆ wss 3895   ⊊ wpss 4013

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956  df-ss 3896  df-pss 4014

This theorem is used by:  psseq1i  4019  psseq1d  4022  psstr  4035  sspsstr  4036  brrpssg  7741  sorpssuni  7748  pssnn  9187  marypha1lem  9428  infeq5i  9640  infpss  10297  fin4i  10379  isfin2-2  10400  zornn0g  10586  ttukeylem7  10596  elnp  11075  elnpi  11076  ltprord  11118  pgpfac1lem1  20295  pgpfac1lem5  20300  pgpfac1  20301  pgpfaclem2  20303  pgpfac  20305  islbs3  21438  alexsubALTlem4  24374  wilthlem2  27401  spansncv  32260  cvbr  32889  cvcon3  32891  cvnbtwn  32893  dfon2lem3  36639  dfon2lem4  36640  dfon2lem5  36641  dfon2lem6  36642  dfon2lem7  36643  dfon2lem8  36644  dfon2  36646  findcard4  38725  lcvbr  40171  lcvnbtwn  40175  mapdcv  42810