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  9185  marypha1lem  9426  infeq5i  9638  infpss  10295  fin4i  10377  isfin2-2  10398  zornn0g  10584  ttukeylem7  10594  elnp  11073  elnpi  11074  ltprord  11116  pgpfac1lem1  20291  pgpfac1lem5  20296  pgpfac1  20297  pgpfaclem2  20299  pgpfac  20301  islbs3  21434  alexsubALTlem4  24370  wilthlem2  27397  spansncv  32256  cvbr  32885  cvcon3  32887  cvnbtwn  32889  dfon2lem3  36590  dfon2lem4  36591  dfon2lem5  36592  dfon2lem6  36593  dfon2lem7  36594  dfon2lem8  36595  dfon2  36597  findcard4  38676  lcvbr  40122  lcvnbtwn  40126  mapdcv  42761