Theorem psseq2 4041

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

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

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929  df-ss 3919  df-pss 3922

This theorem is referenced by:  psseq2i  4043  psseq2d  4046  psssstr  4059  brrpssg  7658  sorpssint  7666  pssnn  9078  php  9116  isfin4  10185  fin2i2  10206  elnp  10875  elnpi  10876  ltprord  10918  pgpfac1lem1  19986  pgpfac1lem5  19991  lbsextlem4  21096  alexsubALTlem4  23963  spansncv  31628  cvbr  32257  cvcon3  32259  cvnbtwn  32261  cvbr4i  32342  ssdifidlprm  33418  ssmxidl  33434  dfon2lem6  35821  dfon2lem7  35822  dfon2lem8  35823  dfon2  35825  lcvbr  39059  lcvnbtwn  39063  lsatcv0  39069  lsat0cv  39071  islshpcv  39091  mapdcv  41698  pssn0  42259