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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3660 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 2886 . . 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:  psseq2i  3730  psseq2d  3733  psssstr  3746  brrpssg  6981  sorpssint  6989  php  8185  php2  8186  pssnn  8219  isfin4  9157  fin2i2  9178  elnp  9847  elnpi  9848  ltprord  9890  pgpfac1lem1  18519  pgpfac1lem5  18524  lbsextlem4  19209  alexsubALTlem4  21901  spansncv  28640  cvbr  29269  cvcon3  29271  cvnbtwn  29273  cvbr4i  29354  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2  31821  lcvbr  34626  lcvnbtwn  34630  lsatcv0  34636  lsat0cv  34638  islshpcv  34658  mapdcv  37266
  Copyright terms: Public domain W3C validator