Theorem psseq2 4043

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2932   ⊆ wss 3901   ⊊ wpss 3902

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933  df-ss 3918  df-pss 3921

This theorem is referenced by:  psseq2i  4045  psseq2d  4048  psssstr  4061  brrpssg  7670  sorpssint  7678  pssnn  9093  php  9131  isfin4  10207  fin2i2  10228  elnp  10898  elnpi  10899  ltprord  10941  pgpfac1lem1  20005  pgpfac1lem5  20010  lbsextlem4  21116  alexsubALTlem4  23994  spansncv  31728  cvbr  32357  cvcon3  32359  cvnbtwn  32361  cvbr4i  32442  ssdifidlprm  33539  ssmxidl  33555  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon2  35984  lcvbr  39277  lcvnbtwn  39281  lsatcv0  39287  lsat0cv  39289  islshpcv  39309  mapdcv  41916  pssn0  42479  nthrucw  47126