Theorem psseq1 4044

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ≠ wne 2933   ⊆ wss 3903   ⊊ wpss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934  df-ss 3920  df-pss 3923

This theorem is referenced by:  psseq1i  4046  psseq1d  4049  psstr  4061  sspsstr  4062  brrpssg  7680  sorpssuni  7687  pssnn  9105  marypha1lem  9348  infeq5i  9557  infpss  10138  fin4i  10220  isfin2-2  10241  zornn0g  10427  ttukeylem7  10437  elnp  10910  elnpi  10911  ltprord  10953  pgpfac1lem1  20017  pgpfac1lem5  20022  pgpfac1  20023  pgpfaclem2  20025  pgpfac  20027  islbs3  21122  alexsubALTlem4  24006  wilthlem2  27047  spansncv  31740  cvbr  32369  cvcon3  32371  cvnbtwn  32373  dfon2lem3  35996  dfon2lem4  35997  dfon2lem5  35998  dfon2lem6  35999  dfon2lem7  36000  dfon2lem8  36001  dfon2  36003  lcvbr  39391  lcvnbtwn  39395  mapdcv  42030  nthrucw  47238