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

Theorem ssiun2s 4500
 Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
Hypothesis
Ref Expression
ssiun2s.1 (𝑥 = 𝐶𝐵 = 𝐷)
Assertion
Ref Expression
ssiun2s (𝐶𝐴𝐷 𝑥𝐴 𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem ssiun2s
StepHypRef Expression
1 nfcv 2751 . 2 𝑥𝐶
2 nfcv 2751 . . 3 𝑥𝐷
3 nfiu1 4486 . . 3 𝑥 𝑥𝐴 𝐵
42, 3nfss 3561 . 2 𝑥 𝐷 𝑥𝐴 𝐵
5 ssiun2s.1 . . 3 (𝑥 = 𝐶𝐵 = 𝐷)
65sseq1d 3595 . 2 (𝑥 = 𝐶 → (𝐵 𝑥𝐴 𝐵𝐷 𝑥𝐴 𝐵))
7 ssiun2 4499 . 2 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
81, 4, 6, 7vtoclgaf 3244 1 (𝐶𝐴𝐷 𝑥𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  ∪ ciun 4455 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457 This theorem is referenced by:  onfununi  7325  oaordi  7513  omordi  7533  dffi3  8220  alephordi  8780  domtriomlem  9147  pwxpndom2  9366  wunex2  9439  imasaddvallem  16012  imasvscaval  16021  iundisj2  23124  voliunlem1  23125  volsup  23131  iundisj2fi  28943  bnj906  30254  bnj1137  30317  bnj1408  30358  cvmliftlem10  30530  cvmliftlem13  30532  sstotbnd2  32743  mapdrvallem3  35953  fvmptiunrelexplb0d  36995  fvmptiunrelexplb1d  36997  corclrcl  37018  trclrelexplem  37022  corcltrcl  37050  cotrclrcl  37053  iunincfi  38300  iundjiunlem  39352  caratheodorylem1  39416  ovnhoilem1  39491
 Copyright terms: Public domain W3C validator