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

Theorem ssiun2 4956
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 3223 . . . 4 ((𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦𝐵)
21ex 416 . . 3 (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦𝐵))
3 eliun 4908 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
42, 3syl6ibr 255 . 2 (𝑥𝐴 → (𝑦𝐵𝑦 𝑥𝐴 𝐵))
54ssrdv 3907 1 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  wrex 3062  wss 3866   ciun 4904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-iun 4906
This theorem is referenced by:  ssiun2s  4957  disjxiun  5050  triun  5174  iunopeqop  5404  ixpf  8601  ixpiunwdom  9206  trpredrec  9342  r1sdom  9390  r1val1  9402  rankuni2b  9469  rankval4  9483  cplem1  9505  domtriomlem  10056  ac6num  10093  iunfo  10153  iundom2g  10154  pwfseqlem3  10274  inar1  10389  tskuni  10397  iunconnlem  22324  ptclsg  22512  ovoliunlem1  24399  limciun  24791  ssiun2sf  30618  djussxp2  30704  suppovss  30737  bnj906  32623  bnj999  32651  bnj1014  32654  bnj1408  32729  rdgssun  35286  cpcolld  41549  iunmapss  42428  ssmapsn  42429  sge0iunmpt  43631  sge0iun  43632  voliunsge0lem  43685  omeiunltfirp  43732
  Copyright terms: Public domain W3C validator