Theorem psseq1 3836

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ≠ wne 2932   ⊆ wss 3715   ⊊ wpss 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ne 2933  df-in 3722  df-ss 3729  df-pss 3731

This theorem is referenced by:  psseq1i  3838  psseq1d  3841  psstr  3853  sspsstr  3854  brrpssg  7104  sorpssuni  7111  pssnn  8343  marypha1lem  8504  infeq5i  8706  infpss  9231  fin4i  9312  isfin2-2  9333  zornn0g  9519  ttukeylem7  9529  elnp  10001  elnpi  10002  ltprord  10044  pgpfac1lem1  18673  pgpfac1lem5  18678  pgpfac1  18679  pgpfaclem2  18681  pgpfac  18683  islbs3  19357  alexsubALTlem4  22055  wilthlem2  24994  spansncv  28821  cvbr  29450  cvcon3  29452  cvnbtwn  29454  dfon2lem3  31995  dfon2lem4  31996  dfon2lem5  31997  dfon2lem6  31998  dfon2lem7  31999  dfon2lem8  32000  dfon2  32002  lcvbr  34811  lcvnbtwn  34815  mapdcv  37451