Theorem psseq2 4046

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ≠ wne 2958   ⊆ wss 3906   ⊊ wpss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959  df-ss 3923  df-pss 3926

This theorem is referenced by:  psseq2i  4048  psseq2d  4051  psssstr  4065  brrpssg  7724  sorpssint  7732  pssnn  9154  php  9192  isfin4  10282  fin2i2  10303  elnp  10973  elnpi  10974  ltprord  11016  pgpfac1lem1  20147  pgpfac1lem5  20152  lbsextlem4  21266  ssdifidlprm  21467  alexsubALTlem4  24188  spansncv  31983  cvbr  32612  cvcon3  32614  cvnbtwn  32616  cvbr4i  32697  ssmxidl  33735  dfon2lem6  36256  dfon2lem7  36257  dfon2lem8  36258  dfon2  36260  lcvbr  39773  lcvnbtwn  39777  lsatcv0  39783  lsat0cv  39785  islshpcv  39805  mapdcv  42412  pssn0  42976  nthrucw  47582