Theorem psseq1 4039

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 3956	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2991	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3918	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3918	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ≠ wne 2929   ⊆ wss 3898   ⊊ wpss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930  df-ss 3915  df-pss 3918

This theorem is referenced by:  psseq1i  4041  psseq1d  4044  psstr  4056  sspsstr  4057  brrpssg  7664  sorpssuni  7671  pssnn  9085  marypha1lem  9324  infeq5i  9533  infpss  10114  fin4i  10196  isfin2-2  10217  zornn0g  10403  ttukeylem7  10413  elnp  10885  elnpi  10886  ltprord  10928  pgpfac1lem1  19990  pgpfac1lem5  19995  pgpfac1  19996  pgpfaclem2  19998  pgpfac  20000  islbs3  21094  alexsubALTlem4  23966  wilthlem2  27007  spansncv  31635  cvbr  32264  cvcon3  32266  cvnbtwn  32268  dfon2lem3  35848  dfon2lem4  35849  dfon2lem5  35850  dfon2lem6  35851  dfon2lem7  35852  dfon2lem8  35853  dfon2  35855  lcvbr  39140  lcvnbtwn  39144  mapdcv  41779  nthrucw  47008