Theorem psseq1 4018

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 3942	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 3005	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3902	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3902	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ≠ wne 2942   ⊆ wss 3883   ⊊ wpss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-in 3890  df-ss 3900  df-pss 3902

This theorem is referenced by:  psseq1i  4020  psseq1d  4023  psstr  4035  sspsstr  4036  brrpssg  7556  sorpssuni  7563  pssnn  8913  pssnnOLD  8969  marypha1lem  9122  infeq5i  9324  infpss  9904  fin4i  9985  isfin2-2  10006  zornn0g  10192  ttukeylem7  10202  elnp  10674  elnpi  10675  ltprord  10717  pgpfac1lem1  19592  pgpfac1lem5  19597  pgpfac1  19598  pgpfaclem2  19600  pgpfac  19602  islbs3  20332  alexsubALTlem4  23109  wilthlem2  26123  spansncv  29916  cvbr  30545  cvcon3  30547  cvnbtwn  30549  dfon2lem3  33667  dfon2lem4  33668  dfon2lem5  33669  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  lcvbr  36962  lcvnbtwn  36966  mapdcv  39601