Theorem psseq2 3856

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 3787	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3000	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 624	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3748	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3748	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 305	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1652   ≠ wne 2937   ⊆ wss 3732   ⊊ wpss 3733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ne 2938  df-in 3739  df-ss 3746  df-pss 3748

This theorem is referenced by:  psseq2i  3858  psseq2d  3861  psssstr  3874  brrpssg  7137  sorpssint  7145  php  8351  php2  8352  pssnn  8385  isfin4  9372  fin2i2  9393  elnp  10062  elnpi  10063  ltprord  10105  pgpfac1lem1  18740  pgpfac1lem5  18745  lbsextlem4  19435  alexsubALTlem4  22133  spansncv  28968  cvbr  29597  cvcon3  29599  cvnbtwn  29601  cvbr4i  29682  dfon2lem6  32136  dfon2lem7  32137  dfon2lem8  32138  dfon2  32140  lcvbr  34977  lcvnbtwn  34981  lsatcv0  34987  lsat0cv  34989  islshpcv  35009  mapdcv  37616  pssn0  37927