Theorem psseq2 4040

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2929   ⊆ wss 3898   ⊊ wpss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930  df-ss 3915  df-pss 3918

This theorem is referenced by:  psseq2i  4042  psseq2d  4045  psssstr  4058  brrpssg  7664  sorpssint  7672  pssnn  9085  php  9123  isfin4  10195  fin2i2  10216  elnp  10885  elnpi  10886  ltprord  10928  pgpfac1lem1  19990  pgpfac1lem5  19995  lbsextlem4  21100  alexsubALTlem4  23966  spansncv  31635  cvbr  32264  cvcon3  32266  cvnbtwn  32268  cvbr4i  32349  ssdifidlprm  33430  ssmxidl  33446  dfon2lem6  35851  dfon2lem7  35852  dfon2lem8  35853  dfon2  35855  lcvbr  39140  lcvnbtwn  39144  lsatcv0  39150  lsat0cv  39152  islshpcv  39172  mapdcv  41779  pssn0  42345  nthrucw  47008