Theorem psseq1 4043

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 3963	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2987	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3925	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3925	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3905   ⊊ wpss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926  df-ss 3922  df-pss 3925

This theorem is referenced by:  psseq1i  4045  psseq1d  4048  psstr  4060  sspsstr  4061  brrpssg  7665  sorpssuni  7672  pssnn  9092  marypha1lem  9342  infeq5i  9551  infpss  10129  fin4i  10211  isfin2-2  10232  zornn0g  10418  ttukeylem7  10428  elnp  10900  elnpi  10901  ltprord  10943  pgpfac1lem1  19973  pgpfac1lem5  19978  pgpfac1  19979  pgpfaclem2  19981  pgpfac  19983  islbs3  21080  alexsubALTlem4  23953  wilthlem2  26995  spansncv  31615  cvbr  32244  cvcon3  32246  cvnbtwn  32248  dfon2lem3  35758  dfon2lem4  35759  dfon2lem5  35760  dfon2lem6  35761  dfon2lem7  35762  dfon2lem8  35763  dfon2  35765  lcvbr  38999  lcvnbtwn  39003  mapdcv  41639