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

Theorem ssequn1 3816
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 212 . . . 4 ((𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
2 pm4.72 938 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵 ↔ (𝑥𝐴𝑥𝐵)))
3 elun 3786 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43bibi1i 327 . . . 4 ((𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥𝐵))
51, 2, 43bitr4i 292 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
65albii 1787 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
7 dfss2 3624 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
8 dfcleq 2645 . 2 ((𝐴𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) ↔ 𝑥𝐵))
96, 7, 83bitr4i 292 1 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wal 1521   = wceq 1523  wcel 2030  cun 3605  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621
This theorem is referenced by:  ssequn2  3819  undif  4082  uniop  5006  pwssun  5049  unisuc  5839  ordssun  5865  ordequn  5866  onun2i  5881  funiunfv  6546  sorpssun  6986  ordunpr  7068  onuninsuci  7082  domss2  8160  sucdom2  8197  findcard2s  8242  rankopb  8753  ranksuc  8766  kmlem11  9020  fin1a2lem10  9269  trclublem  13780  trclubi  13781  trclub  13783  reltrclfv  13802  modfsummods  14569  cvgcmpce  14594  mreexexlem3d  16353  dprd2da  18487  dpjcntz  18497  dpjdisj  18498  dpjlsm  18499  dpjidcl  18503  ablfac1eu  18518  perfcls  21217  dfconn2  21270  comppfsc  21383  llycmpkgen2  21401  trfil2  21738  fixufil  21773  tsmsres  21994  ustssco  22065  ustuqtop1  22092  xrge0gsumle  22683  volsup  23370  mbfss  23458  itg2cnlem2  23574  iblss2  23617  vieta1lem2  24111  amgm  24762  wilthlem2  24840  ftalem3  24846  rpvmasum2  25246  iuninc  29505  hgt750lemb  30862  rankaltopb  32211  hfun  32410  nacsfix  37592  fvnonrel  38220  rclexi  38239  rtrclex  38241  trclubgNEW  38242  trclubNEW  38243  dfrtrcl5  38253  trrelsuperrel2dg  38280  iunrelexp0  38311  corcltrcl  38348  isotone1  38663  aacllem  42875
  Copyright terms: Public domain W3C validator