Theorem psseq1 4041

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958  df-ss 3919  df-pss 3922

This theorem is used by:  psseq1i  4043  psseq1d  4046  psstr  4059  sspsstr  4060  brrpssg  7730  sorpssuni  7737  pssnn  9167  marypha1lem  9407  infeq5i  9619  infpss  10222  fin4i  10304  isfin2-2  10325  zornn0g  10511  ttukeylem7  10521  elnp  11000  elnpi  11001  ltprord  11043  pgpfac1lem1  20209  pgpfac1lem5  20214  pgpfac1  20215  pgpfaclem2  20217  pgpfac  20219  islbs3  21348  alexsubALTlem4  24282  wilthlem2  27313  spansncv  32142  cvbr  32771  cvcon3  32773  cvnbtwn  32775  dfon2lem3  36370  dfon2lem4  36371  dfon2lem5  36372  dfon2lem6  36373  dfon2lem7  36374  dfon2lem8  36375  dfon2  36377  findcard4  38471  lcvbr  39902  lcvnbtwn  39906  mapdcv  42541