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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3659 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 2885 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 747 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3623 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3623 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator