MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psseq1 Structured version   Visualization version   GIF version

Theorem psseq1 4018
Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
psseq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3943 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3052 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 633 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3903 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3903 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 317 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wne 2990  wss 3884  wpss 3885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-v 3446  df-in 3891  df-ss 3901  df-pss 3903
This theorem is referenced by:  psseq1i  4020  psseq1d  4023  psstr  4035  sspsstr  4036  brrpssg  7435  sorpssuni  7442  pssnn  8724  marypha1lem  8885  infeq5i  9087  infpss  9632  fin4i  9713  isfin2-2  9734  zornn0g  9920  ttukeylem7  9930  elnp  10402  elnpi  10403  ltprord  10445  pgpfac1lem1  19192  pgpfac1lem5  19197  pgpfac1  19198  pgpfaclem2  19200  pgpfac  19202  islbs3  19923  alexsubALTlem4  22658  wilthlem2  25657  spansncv  29439  cvbr  30068  cvcon3  30070  cvnbtwn  30072  dfon2lem3  33138  dfon2lem4  33139  dfon2lem5  33140  dfon2lem6  33141  dfon2lem7  33142  dfon2lem8  33143  dfon2  33145  lcvbr  36310  lcvnbtwn  36314  mapdcv  38949
  Copyright terms: Public domain W3C validator