Theorem psseq1 4047

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2961   ⊆ wss 3908   ⊊ wpss 3909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962  df-ss 3925  df-pss 3928

This theorem is used by:  psseq1i  4049  psseq1d  4052  psstr  4065  sspsstr  4066  brrpssg  7735  sorpssuni  7742  pssnn  9163  marypha1lem  9403  infeq5i  9615  infpss  10218  fin4i  10300  isfin2-2  10321  zornn0g  10507  ttukeylem7  10517  elnp  10990  elnpi  10991  ltprord  11033  pgpfac1lem1  20177  pgpfac1lem5  20182  pgpfac1  20183  pgpfaclem2  20185  pgpfac  20187  islbs3  21316  alexsubALTlem4  24244  wilthlem2  27270  spansncv  32042  cvbr  32671  cvcon3  32673  cvnbtwn  32675  dfon2lem3  36295  dfon2lem4  36296  dfon2lem5  36297  dfon2lem6  36298  dfon2lem7  36299  dfon2lem8  36300  dfon2  36302  lcvbr  39835  lcvnbtwn  39839  mapdcv  42474  nthrucw  47647