Theorem psseq2 4066

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2932   ⊆ wss 3926   ⊊ wpss 3927

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ne 2933  df-ss 3943  df-pss 3946

This theorem is referenced by:  psseq2i  4068  psseq2d  4071  psssstr  4084  brrpssg  7717  sorpssint  7725  pssnn  9180  php  9219  phpOLD  9229  php2OLD  9230  isfin4  10309  fin2i2  10330  elnp  10999  elnpi  11000  ltprord  11042  pgpfac1lem1  20055  pgpfac1lem5  20060  lbsextlem4  21120  alexsubALTlem4  23986  spansncv  31580  cvbr  32209  cvcon3  32211  cvnbtwn  32213  cvbr4i  32294  ssdifidlprm  33419  ssmxidl  33435  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  lcvbr  38985  lcvnbtwn  38989  lsatcv0  38995  lsat0cv  38997  islshpcv  39017  mapdcv  41625  pssn0  42224