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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 4020 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3000 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3982 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3982 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wne 2937  wss 3962  wpss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938  df-ss 3979  df-pss 3982
This theorem is referenced by:  psseq1i  4101  psseq1d  4104  psstr  4116  sspsstr  4117  brrpssg  7743  sorpssuni  7750  pssnn  9206  marypha1lem  9470  infeq5i  9673  infpss  10253  fin4i  10335  isfin2-2  10356  zornn0g  10542  ttukeylem7  10552  elnp  11024  elnpi  11025  ltprord  11067  pgpfac1lem1  20108  pgpfac1lem5  20113  pgpfac1  20114  pgpfaclem2  20116  pgpfac  20118  islbs3  21174  alexsubALTlem4  24073  wilthlem2  27126  spansncv  31681  cvbr  32310  cvcon3  32312  cvnbtwn  32314  dfon2lem3  35766  dfon2lem4  35767  dfon2lem5  35768  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  lcvbr  39002  lcvnbtwn  39006  mapdcv  41642
  Copyright terms: Public domain W3C validator