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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3991 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3078 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 630 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3953 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3953 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 315 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wne 3016  wss 3935  wpss 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-ne 3017  df-in 3942  df-ss 3951  df-pss 3953
This theorem is referenced by:  psseq1i  4065  psseq1d  4068  psstr  4080  sspsstr  4081  brrpssg  7440  sorpssuni  7447  pssnn  8725  marypha1lem  8886  infeq5i  9088  infpss  9628  fin4i  9709  isfin2-2  9730  zornn0g  9916  ttukeylem7  9926  elnp  10398  elnpi  10399  ltprord  10441  pgpfac1lem1  19127  pgpfac1lem5  19132  pgpfac1  19133  pgpfaclem2  19135  pgpfac  19137  islbs3  19858  alexsubALTlem4  22588  wilthlem2  25574  spansncv  29358  cvbr  29987  cvcon3  29989  cvnbtwn  29991  dfon2lem3  32928  dfon2lem4  32929  dfon2lem5  32930  dfon2lem6  32931  dfon2lem7  32932  dfon2lem8  32933  dfon2  32935  lcvbr  36039  lcvnbtwn  36043  mapdcv  38678
  Copyright terms: Public domain W3C validator