Theorem psseq2 4091

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2940   ⊆ wss 3951   ⊊ wpss 3952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941  df-ss 3968  df-pss 3971

This theorem is referenced by:  psseq2i  4093  psseq2d  4096  psssstr  4109  brrpssg  7745  sorpssint  7753  pssnn  9208  php  9247  phpOLD  9259  php2OLD  9260  isfin4  10337  fin2i2  10358  elnp  11027  elnpi  11028  ltprord  11070  pgpfac1lem1  20094  pgpfac1lem5  20099  lbsextlem4  21163  alexsubALTlem4  24058  spansncv  31672  cvbr  32301  cvcon3  32303  cvnbtwn  32305  cvbr4i  32386  ssdifidlprm  33486  ssmxidl  33502  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  lcvbr  39022  lcvnbtwn  39026  lsatcv0  39032  lsat0cv  39034  islshpcv  39054  mapdcv  41662  pssn0  42266