Theorem psseq1 4088

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 4008	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3001	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 629	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3968	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3968	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ≠ wne 2938   ⊆ wss 3949   ⊊ wpss 3950

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-in 3956  df-ss 3966  df-pss 3968

This theorem is referenced by:  psseq1i  4090  psseq1d  4093  psstr  4105  sspsstr  4106  brrpssg  7719  sorpssuni  7726  pssnn  9172  pssnnOLD  9269  marypha1lem  9432  infeq5i  9635  infpss  10216  fin4i  10297  isfin2-2  10318  zornn0g  10504  ttukeylem7  10514  elnp  10986  elnpi  10987  ltprord  11029  pgpfac1lem1  19987  pgpfac1lem5  19992  pgpfac1  19993  pgpfaclem2  19995  pgpfac  19997  islbs3  20915  alexsubALTlem4  23776  wilthlem2  26807  spansncv  31171  cvbr  31800  cvcon3  31802  cvnbtwn  31804  dfon2lem3  35059  dfon2lem4  35060  dfon2lem5  35061  dfon2lem6  35062  dfon2lem7  35063  dfon2lem8  35064  dfon2  35066  lcvbr  38196  lcvnbtwn  38200  mapdcv  40836