Theorem psseq1 4046

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ≠ wne 2960   ⊆ wss 3907   ⊊ wpss 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961  df-ss 3924  df-pss 3927

This theorem is referenced by:  psseq1i  4048  psseq1d  4051  psstr  4064  sspsstr  4065  brrpssg  7712  sorpssuni  7719  pssnn  9141  marypha1lem  9381  infeq5i  9593  infpss  10187  fin4i  10270  isfin2-2  10291  zornn0g  10477  ttukeylem7  10487  elnp  10960  elnpi  10961  ltprord  11003  pgpfac1lem1  20137  pgpfac1lem5  20142  pgpfac1  20143  pgpfaclem2  20145  pgpfac  20147  islbs3  21248  alexsubALTlem4  24168  wilthlem2  27191  spansncv  31914  cvbr  32543  cvcon3  32545  cvnbtwn  32547  dfon2lem3  36146  dfon2lem4  36147  dfon2lem5  36148  dfon2lem6  36149  dfon2lem7  36150  dfon2lem8  36151  dfon2  36153  lcvbr  39657  lcvnbtwn  39661  mapdcv  42296  nthrucw  47460