Theorem psseq1 4042

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2932   ⊆ wss 3901   ⊊ wpss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933  df-ss 3918  df-pss 3921

This theorem is referenced by:  psseq1i  4044  psseq1d  4047  psstr  4059  sspsstr  4060  brrpssg  7670  sorpssuni  7677  pssnn  9093  marypha1lem  9336  infeq5i  9545  infpss  10126  fin4i  10208  isfin2-2  10229  zornn0g  10415  ttukeylem7  10425  elnp  10898  elnpi  10899  ltprord  10941  pgpfac1lem1  20005  pgpfac1lem5  20010  pgpfac1  20011  pgpfaclem2  20013  pgpfac  20015  islbs3  21110  alexsubALTlem4  23994  wilthlem2  27035  spansncv  31728  cvbr  32357  cvcon3  32359  cvnbtwn  32361  dfon2lem3  35977  dfon2lem4  35978  dfon2lem5  35979  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon2  35984  lcvbr  39277  lcvnbtwn  39281  mapdcv  41916  nthrucw  47126