Theorem psseq1 4020

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960  df-ss 3901  df-pss 4017

This theorem is used by:  psseq1i  4022  psseq1d  4025  psstr  4038  sspsstr  4039  brrpssg  7765  sorpssuni  7772  pssnn  9212  marypha1lem  9452  infeq5i  9664  infpss  10321  fin4i  10403  isfin2-2  10424  zornn0g  10610  ttukeylem7  10620  elnp  11099  elnpi  11100  ltprord  11142  pgpfac1lem1  20320  pgpfac1lem5  20325  pgpfac1  20326  pgpfaclem2  20328  pgpfac  20330  islbs3  21463  alexsubALTlem4  24399  wilthlem2  27426  spansncv  32285  cvbr  32914  cvcon3  32916  cvnbtwn  32918  elpssex  36635  elpssmo  36636  dfon2lem3  36725  dfon2lem4  36726  dfon2lem5  36727  dfon2lem6  36728  dfon2lem7  36729  dfon2lem8  36730  dfon2  36732  findcard4  38824  lcvbr  40270  lcvnbtwn  40274  mapdcv  42909