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

Theorem ssequn1 4080
Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
ssequn1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)

Proof of Theorem ssequn1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 bicom 225 . . . 4 ((𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
2 pm4.72 949 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
3 elun 4049 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43bibi1i 342 . . . 4 ((𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
51, 2, 43bitr4i 306 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
65albii 1826 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
7 dfss2 3873 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
8 dfcleq 2732 . 2 ((𝐴𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
96, 7, 83bitr4i 306 1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wo 846  wal 1540   = wceq 1542  wcel 2114  cun 3851  wss 3853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-in 3860  df-ss 3870
This theorem is referenced by:  ssequn2  4083  undif  4381  uniop  5382  pwssun  5435  cnvimassrndm  5994  unisuc  6258  ordssun  6281  ordequn  6282  onun2  6286  funiunfv  7030  sorpssun  7486  ordunpr  7572  onuninsuci  7586  sucdom2  8688  domss2  8738  findcard2s  8776  rankopb  9366  ranksuc  9379  kmlem11  9672  fin1a2lem10  9921  trclublem  14456  trclubi  14457  trclub  14459  reltrclfv  14478  modfsummods  15253  cvgcmpce  15278  mreexexlem3d  17032  dprd2da  19295  dpjcntz  19305  dpjdisj  19306  dpjlsm  19307  dpjidcl  19311  ablfac1eu  19326  perfcls  22128  dfconn2  22182  comppfsc  22295  llycmpkgen2  22313  trfil2  22650  fixufil  22685  tsmsres  22907  ustssco  22978  ustuqtop1  23005  xrge0gsumle  23597  volsup  24320  mbfss  24410  itg2cnlem2  24527  iblss2  24570  vieta1lem2  25071  amgm  25740  wilthlem2  25818  ftalem3  25824  rpvmasum2  26260  iuninc  30486  pmtrcnel  30947  pmtrcnelor  30949  hgt750lemb  32218  onunel  33275  noetalem1  33599  madeoldsuc  33722  rankaltopb  33936  hfun  34135  bj-prmoore  34939  nacsfix  40146  fvnonrel  40790  rclexi  40808  rtrclex  40810  trclubgNEW  40811  trclubNEW  40812  dfrtrcl5  40822  trrelsuperrel2dg  40865  iunrelexp0  40896  corcltrcl  40933  isotone1  41244  aacllem  46005
  Copyright terms: Public domain W3C validator