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

Theorem ssequn1 4114
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 221 . . . 4 ((𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
2 pm4.72 947 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
3 elun 4083 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43bibi1i 339 . . . 4 ((𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
51, 2, 43bitr4i 303 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
65albii 1822 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
7 dfss2 3907 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
8 dfcleq 2731 . 2 ((𝐴𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
96, 7, 83bitr4i 303 1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 844  wal 1537   = wceq 1539  wcel 2106  cun 3885  wss 3887
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904
This theorem is referenced by:  ssequn2  4117  undif  4415  uniop  5429  pwssun  5485  cnvimassrndm  6055  unisuc  6342  ordssun  6365  ordequn  6366  onun2  6370  funiunfv  7121  sorpssun  7583  ordunpr  7673  onuninsuci  7687  sucdom2OLD  8869  domss2  8923  findcard2s  8948  sucdom2  8989  rankopb  9610  ranksuc  9623  kmlem11  9916  fin1a2lem10  10165  trclublem  14706  trclubi  14707  trclub  14709  reltrclfv  14728  modfsummods  15505  cvgcmpce  15530  mreexexlem3d  17355  dprd2da  19645  dpjcntz  19655  dpjdisj  19656  dpjlsm  19657  dpjidcl  19661  ablfac1eu  19676  perfcls  22516  dfconn2  22570  comppfsc  22683  llycmpkgen2  22701  trfil2  23038  fixufil  23073  tsmsres  23295  ustssco  23366  ustuqtop1  23393  xrge0gsumle  23996  volsup  24720  mbfss  24810  itg2cnlem2  24927  iblss2  24970  vieta1lem2  25471  amgm  26140  wilthlem2  26218  ftalem3  26224  rpvmasum2  26660  iuninc  30900  pmtrcnel  31358  pmtrcnelor  31360  hgt750lemb  32636  onunel  33689  noetalem1  33944  madeoldsuc  34067  rankaltopb  34281  hfun  34480  bj-prmoore  35286  nacsfix  40534  nlimsuc  41048  fvnonrel  41205  rclexi  41223  rtrclex  41225  trclubgNEW  41226  trclubNEW  41227  dfrtrcl5  41237  trrelsuperrel2dg  41279  iunrelexp0  41310  corcltrcl  41347  isotone1  41658  aacllem  46505
  Copyright terms: Public domain W3C validator