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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3876 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 3023 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2anbi12d 622 . 2 (𝐴 = 𝐵 → ((𝐶𝐴𝐶𝐴) ↔ (𝐶𝐵𝐶𝐵)))
4 df-pss 3838 . 2 (𝐶𝐴 ↔ (𝐶𝐴𝐶𝐴))
5 df-pss 3838 . 2 (𝐶𝐵 ↔ (𝐶𝐵𝐶𝐵))
63, 4, 53bitr4g 306 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1508  wne 2960  wss 3822  wpss 3823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-ne 2961  df-in 3829  df-ss 3836  df-pss 3838
This theorem is referenced by:  psseq2i  3950  psseq2d  3953  psssstr  3966  brrpssg  7267  sorpssint  7275  php  8495  php2  8496  pssnn  8529  isfin4  9515  fin2i2  9536  elnp  10205  elnpi  10206  ltprord  10248  pgpfac1lem1  18958  pgpfac1lem5  18963  lbsextlem4  19667  alexsubALTlem4  22377  spansncv  29226  cvbr  29855  cvcon3  29857  cvnbtwn  29859  cvbr4i  29940  dfon2lem6  32590  dfon2lem7  32591  dfon2lem8  32592  dfon2  32594  lcvbr  35639  lcvnbtwn  35643  lsatcv0  35649  lsat0cv  35651  islshpcv  35671  mapdcv  38278  pssn0  38596
  Copyright terms: Public domain W3C validator