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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3787 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 3000 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2anbi12d 624 . 2 (𝐴 = 𝐵 → ((𝐶𝐴𝐶𝐴) ↔ (𝐶𝐵𝐶𝐵)))
4 df-pss 3748 . 2 (𝐶𝐴 ↔ (𝐶𝐴𝐶𝐴))
5 df-pss 3748 . 2 (𝐶𝐵 ↔ (𝐶𝐵𝐶𝐵))
63, 4, 53bitr4g 305 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wne 2937  wss 3732  wpss 3733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ne 2938  df-in 3739  df-ss 3746  df-pss 3748
This theorem is referenced by:  psseq2i  3858  psseq2d  3861  psssstr  3874  brrpssg  7137  sorpssint  7145  php  8351  php2  8352  pssnn  8385  isfin4  9372  fin2i2  9393  elnp  10062  elnpi  10063  ltprord  10105  pgpfac1lem1  18740  pgpfac1lem5  18745  lbsextlem4  19435  alexsubALTlem4  22133  spansncv  28968  cvbr  29597  cvcon3  29599  cvnbtwn  29601  cvbr4i  29682  dfon2lem6  32136  dfon2lem7  32137  dfon2lem8  32138  dfon2  32140  lcvbr  34977  lcvnbtwn  34981  lsatcv0  34987  lsat0cv  34989  islshpcv  35009  mapdcv  37616  pssn0  37927
  Copyright terms: Public domain W3C validator