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

Theorem ssequn2 3778
Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
Assertion
Ref Expression
ssequn2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)

Proof of Theorem ssequn2
StepHypRef Expression
1 ssequn1 3775 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 uncom 3749 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2625 . 2 ((𝐴𝐵) = 𝐵 ↔ (𝐵𝐴) = 𝐵)
41, 3bitri 264 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481  cun 3565  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-in 3574  df-ss 3581
This theorem is referenced by:  unabs  3846  tppreqb  4327  pwssun  5010  pwundif  5011  relresfld  5650  ordssun  5815  ordequn  5816  oneluni  5828  fsnunf  6436  sorpssun  6929  ordunpr  7011  fodomr  8096  enp1ilem  8179  pwfilem  8245  brwdom2  8463  sucprcreg  8491  dfacfin7  9206  hashbclem  13219  incexclem  14549  ramub1lem1  15711  ramub1lem2  15712  mreexmrid  16284  lspun0  18992  lbsextlem4  19142  cldlp  20935  ordtuni  20975  lfinun  21309  cldsubg  21895  trust  22014  nulmbl2  23285  limcmpt2  23629  cnplimc  23632  dvreslem  23654  dvaddbr  23682  dvmulbr  23683  lhop  23760  plypf1  23949  coeeulem  23961  coeeu  23962  coef2  23968  rlimcnp  24673  ex-un  27251  shs0i  28278  chj0i  28284  disjun0  29380  ffsrn  29478  difioo  29518  eulerpartlemt  30407  subfacp1lem1  31135  cvmscld  31229  mthmpps  31453  refssfne  32328  topjoin  32335  poimirlem3  33383  poimirlem28  33408  rntrclfvOAI  37073  istopclsd  37082  nacsfix  37094  diophrw  37141  clcnvlem  37749  cnvrcl0  37751  dmtrcl  37753  rntrcl  37754  iunrelexp0  37813  dmtrclfvRP  37841  rntrclfv  37843  cotrclrcl  37853  clsk3nimkb  38158  limciccioolb  39653  limcicciooub  39669  ioccncflimc  39861  icocncflimc  39865  stoweidlem44  40024  dirkercncflem3  40085  fourierdlem62  40148  ismeannd  40447
  Copyright terms: Public domain W3C validator