Theorem psseq1 4028

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 3947	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2997	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 638	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3910	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3910	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ≠ wne 2935   ⊆ wss 3890   ⊊ wpss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936  df-ss 3907  df-pss 3910

This theorem is referenced by:  psseq1i  4030  psseq1d  4033  psstr  4045  sspsstr  4046  brrpssg  7675  sorpssuni  7682  pssnn  9100  marypha1lem  9343  infeq5i  9555  infpss  10136  fin4i  10218  isfin2-2  10239  zornn0g  10425  ttukeylem7  10435  elnp  10908  elnpi  10909  ltprord  10951  pgpfac1lem1  20049  pgpfac1lem5  20054  pgpfac1  20055  pgpfaclem2  20057  pgpfac  20059  islbs3  21155  alexsubALTlem4  24040  wilthlem2  27057  spansncv  31749  cvbr  32378  cvcon3  32380  cvnbtwn  32382  dfon2lem3  36018  dfon2lem4  36019  dfon2lem5  36020  dfon2lem6  36021  dfon2lem7  36022  dfon2lem8  36023  dfon2  36025  lcvbr  39520  lcvnbtwn  39524  mapdcv  42159  nthrucw  47338