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

Theorem ssequn1 4160
 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 223 . . . 4 ((𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
2 pm4.72 945 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
3 elun 4129 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43bibi1i 340 . . . 4 ((𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
51, 2, 43bitr4i 304 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
65albii 1813 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
7 dfss2 3959 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
8 dfcleq 2820 . 2 ((𝐴𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
96, 7, 83bitr4i 304 1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 843  ∀wal 1528   = wceq 1530   ∈ wcel 2107   ∪ cun 3938   ⊆ wss 3940 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-in 3947  df-ss 3956 This theorem is referenced by:  ssequn2  4163  undif  4433  uniop  5402  pwssun  5454  unisuc  6266  ordssun  6289  ordequn  6290  onun2i  6305  funiunfv  7003  sorpssun  7450  ordunpr  7534  onuninsuci  7548  domss2  8670  sucdom2  8708  findcard2s  8753  rankopb  9275  ranksuc  9288  kmlem11  9580  fin1a2lem10  9825  trclublem  14350  trclubi  14351  trclub  14353  reltrclfv  14372  modfsummods  15143  cvgcmpce  15168  mreexexlem3d  16912  dprd2da  19100  dpjcntz  19110  dpjdisj  19111  dpjlsm  19112  dpjidcl  19116  ablfac1eu  19131  perfcls  21908  dfconn2  21962  comppfsc  22075  llycmpkgen2  22093  trfil2  22430  fixufil  22465  tsmsres  22686  ustssco  22757  ustuqtop1  22784  xrge0gsumle  23375  volsup  24091  mbfss  24181  itg2cnlem2  24297  iblss2  24340  vieta1lem2  24834  amgm  25501  wilthlem2  25579  ftalem3  25585  rpvmasum2  26021  iuninc  30246  pmtrcnel  30666  pmtrcnelor  30668  hgt750lemb  31832  rankaltopb  33343  hfun  33542  nacsfix  39193  fvnonrel  39841  rclexi  39859  rtrclex  39861  trclubgNEW  39862  trclubNEW  39863  dfrtrcl5  39873  trrelsuperrel2dg  39900  iunrelexp0  39931  corcltrcl  39968  isotone1  40282  aacllem  44804
 Copyright terms: Public domain W3C validator