Theorem psseq2 4032

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
psseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 3949	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 2996	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3910	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3910	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

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

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 3907  df-pss 3910

This theorem is referenced by:  psseq2i  4034  psseq2d  4037  psssstr  4050  brrpssg  7672  sorpssint  7680  pssnn  9096  php  9134  isfin4  10210  fin2i2  10231  elnp  10901  elnpi  10902  ltprord  10944  pgpfac1lem1  20042  pgpfac1lem5  20047  lbsextlem4  21151  alexsubALTlem4  24025  spansncv  31739  cvbr  32368  cvcon3  32370  cvnbtwn  32372  cvbr4i  32453  ssdifidlprm  33533  ssmxidl  33549  dfon2lem6  35984  dfon2lem7  35985  dfon2lem8  35986  dfon2  35988  lcvbr  39481  lcvnbtwn  39485  lsatcv0  39491  lsat0cv  39493  islshpcv  39513  mapdcv  42120  pssn0  42682  nthrucw  47332