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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3610 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 2858 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 746 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3576 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3576 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wne 2796  wss 3560  wpss 3561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-ne 2797  df-in 3567  df-ss 3574  df-pss 3576
This theorem is referenced by:  psseq1i  3679  psseq1d  3682  psstr  3694  sspsstr  3695  brrpssg  6893  sorpssuni  6900  pssnn  8123  marypha1lem  8284  infeq5i  8478  infpss  8984  fin4i  9065  isfin2-2  9086  zornn0g  9272  ttukeylem7  9282  elnp  9754  elnpi  9755  ltprord  9797  pgpfac1lem1  18389  pgpfac1lem5  18394  pgpfac1  18395  pgpfaclem2  18397  pgpfac  18399  islbs3  19069  alexsubALTlem4  21759  wilthlem2  24690  spansncv  28352  cvbr  28981  cvcon3  28983  cvnbtwn  28985  dfon2lem3  31383  dfon2lem4  31384  dfon2lem5  31385  dfon2lem6  31386  dfon2lem7  31387  dfon2lem8  31388  dfon2  31390  lcvbr  33774  lcvnbtwn  33778  mapdcv  36415
  Copyright terms: Public domain W3C validator