Theorem psseq1 4113

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ≠ wne 2946   ⊆ wss 3976   ⊊ wpss 3977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947  df-ss 3993  df-pss 3996

This theorem is referenced by:  psseq1i  4115  psseq1d  4118  psstr  4130  sspsstr  4131  brrpssg  7760  sorpssuni  7767  pssnn  9234  marypha1lem  9502  infeq5i  9705  infpss  10285  fin4i  10367  isfin2-2  10388  zornn0g  10574  ttukeylem7  10584  elnp  11056  elnpi  11057  ltprord  11099  pgpfac1lem1  20118  pgpfac1lem5  20123  pgpfac1  20124  pgpfaclem2  20126  pgpfac  20128  islbs3  21180  alexsubALTlem4  24079  wilthlem2  27130  spansncv  31685  cvbr  32314  cvcon3  32316  cvnbtwn  32318  dfon2lem3  35749  dfon2lem4  35750  dfon2lem5  35751  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  lcvbr  38977  lcvnbtwn  38981  mapdcv  41617