Theorem psseq1 4022

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
psseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Proof of Theorem psseq1

Step	Hyp	Ref	Expression
1		sseq1 3946	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3006	. . 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:  psseq1i  4024  psseq1d  4027  psstr  4039  sspsstr  4040  brrpssg  7578  sorpssuni  7585  pssnn  8951  pssnnOLD  9040  marypha1lem  9192  infeq5i  9394  infpss  9973  fin4i  10054  isfin2-2  10075  zornn0g  10261  ttukeylem7  10271  elnp  10743  elnpi  10744  ltprord  10786  pgpfac1lem1  19677  pgpfac1lem5  19682  pgpfac1  19683  pgpfaclem2  19685  pgpfac  19687  islbs3  20417  alexsubALTlem4  23201  wilthlem2  26218  spansncv  30015  cvbr  30644  cvcon3  30646  cvnbtwn  30648  dfon2lem3  33761  dfon2lem4  33762  dfon2lem5  33763  dfon2lem6  33764  dfon2lem7  33765  dfon2lem8  33766  dfon2  33768  lcvbr  37035  lcvnbtwn  37039  mapdcv  39674