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

Theorem ssiun2s 4555
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 2762 . 2 𝑥𝐶
2 nfcv 2762 . . 3 𝑥𝐷
3 nfiu1 4541 . . 3 𝑥 𝑥𝐴 𝐵
42, 3nfss 3588 . 2 𝑥 𝐷 𝑥𝐴 𝐵
5 ssiun2s.1 . . 3 (𝑥 = 𝐶𝐵 = 𝐷)
65sseq1d 3624 . 2 (𝑥 = 𝐶 → (𝐵 𝑥𝐴 𝐵𝐷 𝑥𝐴 𝐵))
7 ssiun2 4554 . 2 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
81, 4, 6, 7vtoclgaf 3266 1 (𝐶𝐴𝐷 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  wss 3567   ciun 4511
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-ral 2914  df-rex 2915  df-v 3197  df-in 3574  df-ss 3581  df-iun 4513
This theorem is referenced by:  onfununi  7423  oaordi  7611  omordi  7631  dffi3  8322  alephordi  8882  domtriomlem  9249  pwxpndom2  9472  wunex2  9545  imasaddvallem  16170  imasvscaval  16179  iundisj2  23298  voliunlem1  23299  volsup  23305  iundisj2fi  29530  bnj906  30974  bnj1137  31037  bnj1408  31078  cvmliftlem10  31250  cvmliftlem13  31252  sstotbnd2  33544  mapdrvallem3  36754  fvmptiunrelexplb0d  37795  fvmptiunrelexplb1d  37797  corclrcl  37818  trclrelexplem  37822  corcltrcl  37850  cotrclrcl  37853  iunincfi  39092  iundjiunlem  40439  caratheodorylem1  40503  ovnhoilem1  40578
  Copyright terms: Public domain W3C validator