Theorem psseq1 4038

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1541   ≠ wne 2941   ⊆ wss 3901   ⊊ wpss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-v 3444  df-in 3908  df-ss 3918  df-pss 3920

This theorem is referenced by:  psseq1i  4040  psseq1d  4043  psstr  4055  sspsstr  4056  brrpssg  7644  sorpssuni  7651  pssnn  9037  pssnnOLD  9134  marypha1lem  9294  infeq5i  9497  infpss  10078  fin4i  10159  isfin2-2  10180  zornn0g  10366  ttukeylem7  10376  elnp  10848  elnpi  10849  ltprord  10891  pgpfac1lem1  19771  pgpfac1lem5  19776  pgpfac1  19777  pgpfaclem2  19779  pgpfac  19781  islbs3  20522  alexsubALTlem4  23306  wilthlem2  26323  spansncv  30302  cvbr  30931  cvcon3  30933  cvnbtwn  30935  dfon2lem3  34044  dfon2lem4  34045  dfon2lem5  34046  dfon2lem6  34047  dfon2lem7  34048  dfon2lem8  34049  dfon2  34051  lcvbr  37339  lcvnbtwn  37343  mapdcv  39979