Theorem psseq2 4029

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 3948	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 2998	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 638	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3910	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3910	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ≠ wne 2935   ⊆ wss 3890   ⊊ wpss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936  df-ss 3907  df-pss 3910

This theorem is referenced by:  psseq2i  4031  psseq2d  4034  psssstr  4047  brrpssg  7675  sorpssint  7683  pssnn  9100  php  9138  isfin4  10217  fin2i2  10238  elnp  10908  elnpi  10909  ltprord  10951  pgpfac1lem1  20049  pgpfac1lem5  20054  lbsextlem4  21161  alexsubALTlem4  24040  spansncv  31749  cvbr  32378  cvcon3  32380  cvnbtwn  32382  cvbr4i  32463  ssdifidlprm  33548  ssmxidl  33564  dfon2lem6  36021  dfon2lem7  36022  dfon2lem8  36023  dfon2  36025  lcvbr  39520  lcvnbtwn  39524  lsatcv0  39530  lsat0cv  39532  islshpcv  39552  mapdcv  42159  pssn0  42721  nthrucw  47338