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

Theorem ssequn1 3945
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 213 . . . 4 ((𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
2 pm4.72 972 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
3 elun 3915 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43bibi1i 329 . . . 4 ((𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
51, 2, 43bitr4i 294 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
65albii 1914 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
7 dfss2 3749 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
8 dfcleq 2759 . 2 ((𝐴𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
96, 7, 83bitr4i 294 1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wo 873  wal 1650   = wceq 1652  wcel 2155  cun 3730  wss 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3737  df-in 3739  df-ss 3746
This theorem is referenced by:  ssequn2  3948  undif  4209  uniop  5136  pwssun  5181  unisuc  5984  ordssun  6007  ordequn  6008  onun2i  6023  funiunfv  6698  sorpssun  7142  ordunpr  7224  onuninsuci  7238  domss2  8326  sucdom2  8363  findcard2s  8408  rankopb  8930  ranksuc  8943  kmlem11  9235  fin1a2lem10  9484  trclublem  14021  trclubi  14022  trclub  14024  reltrclfv  14043  modfsummods  14809  cvgcmpce  14834  mreexexlem3d  16572  dprd2da  18708  dpjcntz  18718  dpjdisj  18719  dpjlsm  18720  dpjidcl  18724  ablfac1eu  18739  perfcls  21449  dfconn2  21502  comppfsc  21615  llycmpkgen2  21633  trfil2  21970  fixufil  22005  tsmsres  22226  ustssco  22297  ustuqtop1  22324  xrge0gsumle  22915  volsup  23614  mbfss  23704  itg2cnlem2  23820  iblss2  23863  vieta1lem2  24357  amgm  25008  wilthlem2  25086  ftalem3  25092  rpvmasum2  25492  iuninc  29827  hgt750lemb  31185  rankaltopb  32530  hfun  32729  nacsfix  37953  fvnonrel  38578  rclexi  38597  rtrclex  38599  trclubgNEW  38600  trclubNEW  38601  dfrtrcl5  38611  trrelsuperrel2dg  38638  iunrelexp0  38669  corcltrcl  38706  isotone1  39020  aacllem  43219
  Copyright terms: Public domain W3C validator