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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3767 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 2994 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 749 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3731 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3731 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wne 2932  wss 3715  wpss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ne 2933  df-in 3722  df-ss 3729  df-pss 3731
This theorem is referenced by:  psseq1i  3838  psseq1d  3841  psstr  3853  sspsstr  3854  brrpssg  7104  sorpssuni  7111  pssnn  8343  marypha1lem  8504  infeq5i  8706  infpss  9231  fin4i  9312  isfin2-2  9333  zornn0g  9519  ttukeylem7  9529  elnp  10001  elnpi  10002  ltprord  10044  pgpfac1lem1  18673  pgpfac1lem5  18678  pgpfac1  18679  pgpfaclem2  18681  pgpfac  18683  islbs3  19357  alexsubALTlem4  22055  wilthlem2  24994  spansncv  28821  cvbr  29450  cvcon3  29452  cvnbtwn  29454  dfon2lem3  31995  dfon2lem4  31996  dfon2lem5  31997  dfon2lem6  31998  dfon2lem7  31999  dfon2lem8  32000  dfon2  32002  lcvbr  34811  lcvnbtwn  34815  mapdcv  37451
  Copyright terms: Public domain W3C validator