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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3786 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 2999 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 624 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3748 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3748 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 305 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wne 2937  wss 3732  wpss 3733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ne 2938  df-in 3739  df-ss 3746  df-pss 3748
This theorem is referenced by:  psseq1i  3857  psseq1d  3860  psstr  3872  sspsstr  3873  brrpssg  7137  sorpssuni  7144  pssnn  8385  marypha1lem  8546  infeq5i  8748  infpss  9292  fin4i  9373  isfin2-2  9394  zornn0g  9580  ttukeylem7  9590  elnp  10062  elnpi  10063  ltprord  10105  pgpfac1lem1  18740  pgpfac1lem5  18745  pgpfac1  18746  pgpfaclem2  18748  pgpfac  18750  islbs3  19429  alexsubALTlem4  22133  wilthlem2  25086  spansncv  28903  cvbr  29532  cvcon3  29534  cvnbtwn  29536  dfon2lem3  32065  dfon2lem4  32066  dfon2lem5  32067  dfon2lem6  32068  dfon2lem7  32069  dfon2lem8  32070  dfon2  32072  lcvbr  34909  lcvnbtwn  34913  mapdcv  37548
  Copyright terms: Public domain W3C validator