Theorem psseq2 4023

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ≠ wne 2943   ⊆ wss 3887   ⊊ wpss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-v 3434  df-in 3894  df-ss 3904  df-pss 3906

This theorem is referenced by:  psseq2i  4025  psseq2d  4028  psssstr  4041  brrpssg  7578  sorpssint  7586  pssnn  8951  php  8993  phpOLD  9005  php2OLD  9006  pssnnOLD  9040  isfin4  10053  fin2i2  10074  elnp  10743  elnpi  10744  ltprord  10786  pgpfac1lem1  19677  pgpfac1lem5  19682  lbsextlem4  20423  alexsubALTlem4  23201  spansncv  30015  cvbr  30644  cvcon3  30646  cvnbtwn  30648  cvbr4i  30729  ssmxidl  31642  dfon2lem6  33764  dfon2lem7  33765  dfon2lem8  33766  dfon2  33768  lcvbr  37035  lcvnbtwn  37039  lsatcv0  37045  lsat0cv  37047  islshpcv  37067  mapdcv  39674  pssn0  40202