Theorem psseq2 4003

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 3927	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
2		neeq2 3004	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))
3	1, 2	anbi12d 634	. 2 ⊢ (𝐴 = 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴) ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵)))
4		df-pss 3885	. 2 ⊢ (𝐶 ⊊ 𝐴 ↔ (𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ 𝐴))
5		df-pss 3885	. 2 ⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ 𝐶 ≠ 𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊊ 𝐴 ↔ 𝐶 ⊊ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ≠ wne 2940   ⊆ wss 3866   ⊊ wpss 3867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3410  df-in 3873  df-ss 3883  df-pss 3885

This theorem is referenced by:  psseq2i  4005  psseq2d  4008  psssstr  4021  brrpssg  7513  sorpssint  7521  php  8830  php2  8831  pssnn  8846  pssnnOLD  8895  isfin4  9911  fin2i2  9932  elnp  10601  elnpi  10602  ltprord  10644  pgpfac1lem1  19461  pgpfac1lem5  19466  lbsextlem4  20198  alexsubALTlem4  22947  spansncv  29734  cvbr  30363  cvcon3  30365  cvnbtwn  30367  cvbr4i  30448  ssmxidl  31356  dfon2lem6  33483  dfon2lem7  33484  dfon2lem8  33485  dfon2  33487  lcvbr  36772  lcvnbtwn  36776  lsatcv0  36782  lsat0cv  36784  islshpcv  36804  mapdcv  39411  pssn0  39915