Theorem psseq1 4066

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ≠ wne 3018   ⊆ wss 3938   ⊊ wpss 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ne 3019  df-in 3945  df-ss 3954  df-pss 3956

This theorem is referenced by:  psseq1i  4068  psseq1d  4071  psstr  4083  sspsstr  4084  brrpssg  7453  sorpssuni  7460  pssnn  8738  marypha1lem  8899  infeq5i  9101  infpss  9641  fin4i  9722  isfin2-2  9743  zornn0g  9929  ttukeylem7  9939  elnp  10411  elnpi  10412  ltprord  10454  pgpfac1lem1  19198  pgpfac1lem5  19203  pgpfac1  19204  pgpfaclem2  19206  pgpfac  19208  islbs3  19929  alexsubALTlem4  22660  wilthlem2  25648  spansncv  29432  cvbr  30061  cvcon3  30063  cvnbtwn  30065  dfon2lem3  33032  dfon2lem4  33033  dfon2lem5  33034  dfon2lem6  33035  dfon2lem7  33036  dfon2lem8  33037  dfon2  33039  lcvbr  36159  lcvnbtwn  36163  mapdcv  38798