Theorem psseq1 3988

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ≠ wne 2932   ⊆ wss 3853   ⊊ wpss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-v 3400  df-in 3860  df-ss 3870  df-pss 3872

This theorem is referenced by:  psseq1i  3990  psseq1d  3993  psstr  4005  sspsstr  4006  brrpssg  7491  sorpssuni  7498  pssnn  8824  pssnnOLD  8872  marypha1lem  9027  infeq5i  9229  infpss  9796  fin4i  9877  isfin2-2  9898  zornn0g  10084  ttukeylem7  10094  elnp  10566  elnpi  10567  ltprord  10609  pgpfac1lem1  19415  pgpfac1lem5  19420  pgpfac1  19421  pgpfaclem2  19423  pgpfac  19425  islbs3  20146  alexsubALTlem4  22901  wilthlem2  25905  spansncv  29688  cvbr  30317  cvcon3  30319  cvnbtwn  30321  dfon2lem3  33431  dfon2lem4  33432  dfon2lem5  33433  dfon2lem6  33434  dfon2lem7  33435  dfon2lem8  33436  dfon2  33438  lcvbr  36721  lcvnbtwn  36725  mapdcv  39360