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

Theorem ssiun2 4499
 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 2986 . . . 4 ((𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦𝐵)
21ex 449 . . 3 (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦𝐵))
3 eliun 4460 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
42, 3syl6ibr 241 . 2 (𝑥𝐴 → (𝑦𝐵𝑦 𝑥𝐴 𝐵))
54ssrdv 3574 1 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977  ∃wrex 2897   ⊆ 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:  ssiun2s  4500  disjxiun  4579  disjxiunOLD  4580  triun  4694  iunopeqop  4906  ixpf  7816  ixpiunwdom  8379  r1sdom  8520  r1val1  8532  rankuni2b  8599  rankval4  8613  cplem1  8635  domtriomlem  9147  ac6num  9184  iunfo  9240  iundom2g  9241  pwfseqlem3  9361  inar1  9476  tskuni  9484  iunconlem  21040  ptclsg  21228  ovoliunlem1  23077  limciun  23464  ssiun2sf  28760  bnj906  30254  bnj999  30281  bnj1014  30284  bnj1408  30358  trpredrec  30982  iunmapss  38402  ssmapsn  38403  sge0iunmpt  39311  sge0iun  39312  voliunsge0lem  39365  omeiunltfirp  39409
 Copyright terms: Public domain W3C validator