ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eliun GIF version

Theorem eliun 3702
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem eliun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elex 2619 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 2619 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 2478 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2145 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 2374 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 3700 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 2748 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 653 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1285  wcel 1434  wrex 2354  Vcvv 2610   ciun 3698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-iun 3700
This theorem is referenced by:  iuncom  3704  iuncom4  3705  iunconstm  3706  iuniin  3708  iunss1  3709  ss2iun  3713  dfiun2g  3730  ssiun  3740  ssiun2  3741  iunab  3744  iun0  3754  0iun  3755  iunn0m  3758  iunin2  3761  iundif2ss  3763  iindif2m  3765  iunxsng  3773  iunun  3775  iunxun  3776  iunxiun  3777  iunpwss  3784  triun  3908  iunpw  4257  xpiundi  4444  xpiundir  4445  iunxpf  4532  cnvuni  4569  dmiun  4592  dmuni  4593  rniun  4784  dfco2  4870  dfco2a  4871  coiun  4880  fun11iun  5199  imaiun  5452  eluniimadm  5457  opabex3d  5800  opabex3  5801  smoiun  5971  tfrlemi14d  6003  tfr1onlemres  6019  tfrcllemres  6032
  Copyright terms: Public domain W3C validator