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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 4021 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 3001 . . 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:  psseq2i  4102  psseq2d  4105  psssstr  4118  brrpssg  7743  sorpssint  7751  pssnn  9206  php  9244  phpOLD  9256  php2OLD  9257  isfin4  10334  fin2i2  10355  elnp  11024  elnpi  11025  ltprord  11067  pgpfac1lem1  20108  pgpfac1lem5  20113  lbsextlem4  21180  alexsubALTlem4  24073  spansncv  31681  cvbr  32310  cvcon3  32312  cvnbtwn  32314  cvbr4i  32395  ssdifidlprm  33465  ssmxidl  33481  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  lcvbr  39002  lcvnbtwn  39006  lsatcv0  39012  lsat0cv  39014  islshpcv  39034  mapdcv  41642  pssn0  42244
  Copyright terms: Public domain W3C validator