Theorem psseq1 3677

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ≠ wne 2796   ⊆ wss 3560   ⊊ wpss 3561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-ne 2797  df-in 3567  df-ss 3574  df-pss 3576

This theorem is referenced by:  psseq1i  3679  psseq1d  3682  psstr  3694  sspsstr  3695  brrpssg  6893  sorpssuni  6900  pssnn  8123  marypha1lem  8284  infeq5i  8478  infpss  8984  fin4i  9065  isfin2-2  9086  zornn0g  9272  ttukeylem7  9282  elnp  9754  elnpi  9755  ltprord  9797  pgpfac1lem1  18389  pgpfac1lem5  18394  pgpfac1  18395  pgpfaclem2  18397  pgpfac  18399  islbs3  19069  alexsubALTlem4  21759  wilthlem2  24690  spansncv  28352  cvbr  28981  cvcon3  28983  cvnbtwn  28985  dfon2lem3  31383  dfon2lem4  31384  dfon2lem5  31385  dfon2lem6  31386  dfon2lem7  31387  dfon2lem8  31388  dfon2  31390  lcvbr  33774  lcvnbtwn  33778  mapdcv  36415