Theorem psseq1 4045

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ≠ wne 2958   ⊆ wss 3906   ⊊ wpss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959  df-ss 3923  df-pss 3926

This theorem is referenced by:  psseq1i  4047  psseq1d  4050  psstr  4063  sspsstr  4064  brrpssg  7724  sorpssuni  7731  pssnn  9154  marypha1lem  9394  infeq5i  9606  infpss  10200  fin4i  10283  isfin2-2  10304  zornn0g  10490  ttukeylem7  10500  elnp  10973  elnpi  10974  ltprord  11016  pgpfac1lem1  20147  pgpfac1lem5  20152  pgpfac1  20153  pgpfaclem2  20155  pgpfac  20157  islbs3  21260  alexsubALTlem4  24188  wilthlem2  27211  spansncv  31983  cvbr  32612  cvcon3  32614  cvnbtwn  32616  dfon2lem3  36253  dfon2lem4  36254  dfon2lem5  36255  dfon2lem6  36256  dfon2lem7  36257  dfon2lem8  36258  dfon2  36260  lcvbr  39773  lcvnbtwn  39777  mapdcv  42412  nthrucw  47582