Theorem psseq1 3956

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 3884	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3029	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 621	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3847	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3847	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ≠ wne 2967   ⊆ wss 3831   ⊊ wpss 3832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-ne 2968  df-in 3838  df-ss 3845  df-pss 3847

This theorem is referenced by:  psseq1i  3958  psseq1d  3961  psstr  3973  sspsstr  3974  brrpssg  7271  sorpssuni  7278  pssnn  8533  marypha1lem  8694  infeq5i  8895  infpss  9439  fin4i  9520  isfin2-2  9541  zornn0g  9727  ttukeylem7  9737  elnp  10209  elnpi  10210  ltprord  10252  pgpfac1lem1  18949  pgpfac1lem5  18954  pgpfac1  18955  pgpfaclem2  18957  pgpfac  18959  islbs3  19652  alexsubALTlem4  22365  wilthlem2  25351  spansncv  29214  cvbr  29843  cvcon3  29845  cvnbtwn  29847  dfon2lem3  32550  dfon2lem4  32551  dfon2lem5  32552  dfon2lem6  32553  dfon2lem7  32554  dfon2lem8  32555  dfon2  32557  lcvbr  35602  lcvnbtwn  35606  mapdcv  38241