Theorem psseq1 4043

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 3961	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3018	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 641	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3924	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3924	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ≠ wne 2956   ⊆ wss 3904   ⊊ wpss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957  df-ss 3921  df-pss 3924

This theorem is referenced by:  psseq1i  4045  psseq1d  4048  psstr  4061  sspsstr  4062  brrpssg  7704  sorpssuni  7711  pssnn  9133  marypha1lem  9376  infeq5i  9588  infpss  10169  fin4i  10252  isfin2-2  10273  zornn0g  10459  ttukeylem7  10469  elnp  10942  elnpi  10943  ltprord  10985  pgpfac1lem1  20099  pgpfac1lem5  20104  pgpfac1  20105  pgpfaclem2  20107  pgpfac  20109  islbs3  21205  alexsubALTlem4  24090  wilthlem2  27110  spansncv  31802  cvbr  32431  cvcon3  32433  cvnbtwn  32435  dfon2lem3  36097  dfon2lem4  36098  dfon2lem5  36099  dfon2lem6  36100  dfon2lem7  36101  dfon2lem8  36102  dfon2  36104  lcvbr  39609  lcvnbtwn  39613  mapdcv  42248  nthrucw  47426