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

Theorem ssiun2 4938
 Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ssiun2 (𝑥𝐴𝐵 𝑥𝐴 𝐵)

Proof of Theorem ssiun2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 rspe 3264 . . . 4 ((𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦𝐵)
21ex 416 . . 3 (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦𝐵))
3 eliun 4889 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
42, 3syl6ibr 255 . 2 (𝑥𝐴 → (𝑦𝐵𝑦 𝑥𝐴 𝐵))
54ssrdv 3923 1 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3107   ⊆ wss 3883  ∪ ciun 4885 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3444  df-in 3890  df-ss 3900  df-iun 4887 This theorem is referenced by:  ssiun2s  4939  disjxiun  5031  triun  5153  iunopeqop  5380  ixpf  8485  ixpiunwdom  9056  r1sdom  9205  r1val1  9217  rankuni2b  9284  rankval4  9298  cplem1  9320  domtriomlem  9871  ac6num  9908  iunfo  9968  iundom2g  9969  pwfseqlem3  10089  inar1  10204  tskuni  10212  iunconnlem  22073  ptclsg  22261  ovoliunlem1  24147  limciun  24538  ssiun2sf  30367  djussxp2  30454  suppovss  30487  bnj906  32378  bnj999  32406  bnj1014  32409  bnj1408  32484  trpredrec  33260  rdgssun  34946  cpcolld  41137  iunmapss  42014  ssmapsn  42015  sge0iunmpt  43225  sge0iun  43226  voliunsge0lem  43279  omeiunltfirp  43326
 Copyright terms: Public domain W3C validator