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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3941 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
2 neeq2 3050 . . 3 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2anbi12d 633 . 2 (𝐴 = 𝐵 → ((𝐶𝐴𝐶𝐴) ↔ (𝐶𝐵𝐶𝐵)))
4 df-pss 3900 . 2 (𝐶𝐴 ↔ (𝐶𝐴𝐶𝐴))
5 df-pss 3900 . 2 (𝐶𝐵 ↔ (𝐶𝐵𝐶𝐵))
63, 4, 53bitr4g 317 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ≠ wne 2987   ⊆ wss 3881   ⊊ wpss 3882 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-in 3888  df-ss 3898  df-pss 3900 This theorem is referenced by:  psseq2i  4018  psseq2d  4021  psssstr  4034  brrpssg  7438  sorpssint  7446  php  8692  php2  8693  pssnn  8727  isfin4  9715  fin2i2  9736  elnp  10405  elnpi  10406  ltprord  10448  pgpfac1lem1  19197  pgpfac1lem5  19202  lbsextlem4  19934  alexsubALTlem4  22669  spansncv  29450  cvbr  30079  cvcon3  30081  cvnbtwn  30083  cvbr4i  30164  ssmxidl  31081  dfon2lem6  33182  dfon2lem7  33183  dfon2lem8  33184  dfon2  33186  lcvbr  36357  lcvnbtwn  36361  lsatcv0  36367  lsat0cv  36369  islshpcv  36389  mapdcv  38996  pssn0  39448
 Copyright terms: Public domain W3C validator