Theorem psseq2 3728

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 3660	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 2886	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 747	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3623	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3623	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 303	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ≠ wne 2823   ⊆ wss 3607   ⊊ wpss 3608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ne 2824  df-in 3614  df-ss 3621  df-pss 3623

This theorem is referenced by:  psseq2i  3730  psseq2d  3733  psssstr  3746  brrpssg  6981  sorpssint  6989  php  8185  php2  8186  pssnn  8219  isfin4  9157  fin2i2  9178  elnp  9847  elnpi  9848  ltprord  9890  pgpfac1lem1  18519  pgpfac1lem5  18524  lbsextlem4  19209  alexsubALTlem4  21901  spansncv  28640  cvbr  29269  cvcon3  29271  cvnbtwn  29273  cvbr4i  29354  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2  31821  lcvbr  34626  lcvnbtwn  34630  lsatcv0  34636  lsat0cv  34638  islshpcv  34658  mapdcv  37266