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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3968 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 neeq1 3005 . . 3 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2anbi12d 632 . 2 (𝐴 = 𝐵 → ((𝐴𝐶𝐴𝐶) ↔ (𝐵𝐶𝐵𝐶)))
4 df-pss 3928 . 2 (𝐴𝐶 ↔ (𝐴𝐶𝐴𝐶))
5 df-pss 3928 . 2 (𝐵𝐶 ↔ (𝐵𝐶𝐵𝐶))
63, 4, 53bitr4g 314 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wne 2942  wss 3909  wpss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-v 3446  df-in 3916  df-ss 3926  df-pss 3928
This theorem is referenced by:  psseq1i  4048  psseq1d  4051  psstr  4063  sspsstr  4064  brrpssg  7653  sorpssuni  7660  pssnn  9046  pssnnOLD  9143  marypha1lem  9303  infeq5i  9506  infpss  10087  fin4i  10168  isfin2-2  10189  zornn0g  10375  ttukeylem7  10385  elnp  10857  elnpi  10858  ltprord  10900  pgpfac1lem1  19782  pgpfac1lem5  19787  pgpfac1  19788  pgpfaclem2  19790  pgpfac  19792  islbs3  20539  alexsubALTlem4  23323  wilthlem2  26340  spansncv  30381  cvbr  31010  cvcon3  31012  cvnbtwn  31014  dfon2lem3  34138  dfon2lem4  34139  dfon2lem5  34140  dfon2lem6  34141  dfon2lem7  34142  dfon2lem8  34143  dfon2  34145  lcvbr  37369  lcvnbtwn  37373  mapdcv  40009
  Copyright terms: Public domain W3C validator