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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3967 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3004 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 631 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3927 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3927 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 313 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wne 2941  wss 3908  wpss 3909
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-v 3445  df-in 3915  df-ss 3925  df-pss 3927
This theorem is referenced by:  psseq1i  4047  psseq1d  4050  psstr  4062  sspsstr  4063  brrpssg  7652  sorpssuni  7659  pssnn  9045  pssnnOLD  9142  marypha1lem  9302  infeq5i  9505  infpss  10086  fin4i  10167  isfin2-2  10188  zornn0g  10374  ttukeylem7  10384  elnp  10856  elnpi  10857  ltprord  10899  pgpfac1lem1  19782  pgpfac1lem5  19787  pgpfac1  19788  pgpfaclem2  19790  pgpfac  19792  islbs3  20539  alexsubALTlem4  23323  wilthlem2  26340  spansncv  30393  cvbr  31022  cvcon3  31024  cvnbtwn  31026  dfon2lem3  34150  dfon2lem4  34151  dfon2lem5  34152  dfon2lem6  34153  dfon2lem7  34154  dfon2lem8  34155  dfon2  34157  lcvbr  37378  lcvnbtwn  37382  mapdcv  40018
  Copyright terms: Public domain W3C validator