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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3776 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 3006 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2anbi12d 616 . 2 (𝐴 = 𝐵 → ((𝐶𝐴𝐶𝐴) ↔ (𝐶𝐵𝐶𝐵)))
4 df-pss 3739 . 2 (𝐶𝐴 ↔ (𝐶𝐴𝐶𝐴))
5 df-pss 3739 . 2 (𝐶𝐵 ↔ (𝐶𝐵𝐶𝐵))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wne 2943  wss 3723  wpss 3724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ne 2944  df-in 3730  df-ss 3737  df-pss 3739
This theorem is referenced by:  psseq2i  3847  psseq2d  3850  psssstr  3863  brrpssg  7086  sorpssint  7094  php  8300  php2  8301  pssnn  8334  isfin4  9321  fin2i2  9342  elnp  10011  elnpi  10012  ltprord  10054  pgpfac1lem1  18681  pgpfac1lem5  18686  lbsextlem4  19376  alexsubALTlem4  22074  spansncv  28852  cvbr  29481  cvcon3  29483  cvnbtwn  29485  cvbr4i  29566  dfon2lem6  32029  dfon2lem7  32030  dfon2lem8  32031  dfon2  32033  lcvbr  34830  lcvnbtwn  34834  lsatcv0  34840  lsat0cv  34842  islshpcv  34862  mapdcv  37470  pssn0  37775
  Copyright terms: Public domain W3C validator