Theorem psseq2 4048

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2961   ⊆ wss 3908   ⊊ wpss 3909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962  df-ss 3925  df-pss 3928

This theorem is used by:  psseq2i  4050  psseq2d  4053  psssstr  4067  brrpssg  7735  sorpssint  7743  pssnn  9163  php  9201  isfin4  10299  fin2i2  10320  elnp  10990  elnpi  10991  ltprord  11033  pgpfac1lem1  20177  pgpfac1lem5  20182  lbsextlem4  21322  ssdifidlprm  21523  alexsubALTlem4  24244  spansncv  32042  cvbr  32671  cvcon3  32673  cvnbtwn  32675  cvbr4i  32756  ssmxidl  33788  dfon2lem6  36299  dfon2lem7  36300  dfon2lem8  36301  dfon2  36303  lcvbr  39836  lcvnbtwn  39840  lsatcv0  39846  lsat0cv  39848  islshpcv  39868  mapdcv  42475  pssn0  43039  nthrucw  47648