Theorem psseq1 3727

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 3659	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
2		neeq1 2885	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
3	1, 2	anbi12d 747	. 2 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶) ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶)))
4		df-pss 3623	. 2 ⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐴 ≠ 𝐶))
5		df-pss 3623	. 2 ⊢ (𝐵 ⊊ 𝐶 ↔ (𝐵 ⊆ 𝐶 ∧ 𝐵 ≠ 𝐶))
6	3, 4, 5	3bitr4g 303	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊊ 𝐶 ↔ 𝐵 ⊊ 𝐶))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ≠ wne 2823   ⊆ wss 3607   ⊊ wpss 3608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ne 2824  df-in 3614  df-ss 3621  df-pss 3623

This theorem is referenced by:  psseq1i  3729  psseq1d  3732  psstr  3744  sspsstr  3745  brrpssg  6981  sorpssuni  6988  pssnn  8219  marypha1lem  8380  infeq5i  8571  infpss  9077  fin4i  9158  isfin2-2  9179  zornn0g  9365  ttukeylem7  9375  elnp  9847  elnpi  9848  ltprord  9890  pgpfac1lem1  18519  pgpfac1lem5  18524  pgpfac1  18525  pgpfaclem2  18527  pgpfac  18529  islbs3  19203  alexsubALTlem4  21901  wilthlem2  24840  spansncv  28640  cvbr  29269  cvcon3  29271  cvnbtwn  29273  dfon2lem3  31814  dfon2lem4  31815  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2  31821  lcvbr  34626  lcvnbtwn  34630  mapdcv  37266