Theorem psseq2 4114

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ≠ wne 2946   ⊆ wss 3976   ⊊ wpss 3977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947  df-ss 3993  df-pss 3996

This theorem is referenced by:  psseq2i  4116  psseq2d  4119  psssstr  4132  brrpssg  7760  sorpssint  7768  pssnn  9234  php  9273  phpOLD  9285  php2OLD  9286  isfin4  10366  fin2i2  10387  elnp  11056  elnpi  11057  ltprord  11099  pgpfac1lem1  20118  pgpfac1lem5  20123  lbsextlem4  21186  alexsubALTlem4  24079  spansncv  31685  cvbr  32314  cvcon3  32316  cvnbtwn  32318  cvbr4i  32399  ssdifidlprm  33451  ssmxidl  33467  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  lcvbr  38977  lcvnbtwn  38981  lsatcv0  38987  lsat0cv  38989  islshpcv  39009  mapdcv  41617  pssn0  42220