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

Theorem ssiun2 4697
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 3151 . . . 4 ((𝑥𝐴𝑦𝐵) → ∃𝑥𝐴 𝑦𝐵)
21ex 397 . . 3 (𝑥𝐴 → (𝑦𝐵 → ∃𝑥𝐴 𝑦𝐵))
3 eliun 4658 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
42, 3syl6ibr 242 . 2 (𝑥𝐴 → (𝑦𝐵𝑦 𝑥𝐴 𝐵))
54ssrdv 3758 1 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wrex 3062  wss 3723   ciun 4654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-iun 4656
This theorem is referenced by:  ssiun2s  4698  disjxiun  4783  triun  4899  iunopeqop  5114  ixpf  8082  ixpiunwdom  8650  r1sdom  8799  r1val1  8811  rankuni2b  8878  rankval4  8892  cplem1  8914  domtriomlem  9464  ac6num  9501  iunfo  9561  iundom2g  9562  pwfseqlem3  9682  inar1  9797  tskuni  9805  iunconnlem  21444  ptclsg  21632  ovoliunlem1  23483  limciun  23871  ssiun2sf  29709  bnj906  31331  bnj999  31358  bnj1014  31361  bnj1408  31435  trpredrec  32067  iunmapss  39918  ssmapsn  39919  sge0iunmpt  41145  sge0iun  41146  voliunsge0lem  41199  omeiunltfirp  41246
  Copyright terms: Public domain W3C validator