Theorem psseq2 4018

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 3934	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3018	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 4014	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 4014	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ≠ wne 2955   ⊆ wss 3895   ⊊ wpss 4013

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956  df-ss 3896  df-pss 4014

This theorem is used by:  psseq2i  4020  psseq2d  4023  psssstr  4037  brrpssg  7741  sorpssint  7749  pssnn  9187  php  9225  isfin4  10378  fin2i2  10399  elnp  11075  elnpi  11076  ltprord  11118  pgpfac1lem1  20295  pgpfac1lem5  20300  lbsextlem4  21444  ssdifidlprm  21647  alexsubALTlem4  24374  spansncv  32260  cvbr  32889  cvcon3  32891  cvnbtwn  32893  cvbr4i  32974  ssmxidl  34045  dfon2lem6  36642  dfon2lem7  36643  dfon2lem8  36644  dfon2  36646  findcard4  38725  lcvbr  40171  lcvnbtwn  40175  lsatcv0  40181  lsat0cv  40183  islshpcv  40203  mapdcv  42810  pssn0  43374