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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 4009 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3003 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3971 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3971 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wne 2940  wss 3951  wpss 3952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941  df-ss 3968  df-pss 3971
This theorem is referenced by:  psseq1i  4092  psseq1d  4095  psstr  4107  sspsstr  4108  brrpssg  7745  sorpssuni  7752  pssnn  9208  marypha1lem  9473  infeq5i  9676  infpss  10256  fin4i  10338  isfin2-2  10359  zornn0g  10545  ttukeylem7  10555  elnp  11027  elnpi  11028  ltprord  11070  pgpfac1lem1  20094  pgpfac1lem5  20099  pgpfac1  20100  pgpfaclem2  20102  pgpfac  20104  islbs3  21157  alexsubALTlem4  24058  wilthlem2  27112  spansncv  31672  cvbr  32301  cvcon3  32303  cvnbtwn  32305  dfon2lem3  35786  dfon2lem4  35787  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  lcvbr  39022  lcvnbtwn  39026  mapdcv  41662
  Copyright terms: Public domain W3C validator