Theorem psseq2 4044

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925   ⊆ wss 3905   ⊊ wpss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926  df-ss 3922  df-pss 3925

This theorem is referenced by:  psseq2i  4046  psseq2d  4049  psssstr  4062  brrpssg  7665  sorpssint  7673  pssnn  9092  php  9131  isfin4  10210  fin2i2  10231  elnp  10900  elnpi  10901  ltprord  10943  pgpfac1lem1  19973  pgpfac1lem5  19978  lbsextlem4  21086  alexsubALTlem4  23953  spansncv  31615  cvbr  32244  cvcon3  32246  cvnbtwn  32248  cvbr4i  32329  ssdifidlprm  33405  ssmxidl  33421  dfon2lem6  35761  dfon2lem7  35762  dfon2lem8  35763  dfon2  35765  lcvbr  38999  lcvnbtwn  39003  lsatcv0  39009  lsat0cv  39011  islshpcv  39031  mapdcv  41639  pssn0  42200