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

Theorem eliun 3892
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 2750 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 2750 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 2590 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2240 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 2478 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 3890 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 2886 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 704 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wb 105   = wceq 1353  wcel 2148  wrex 2456  Vcvv 2739   ciun 3888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-iun 3890
This theorem is referenced by:  iuncom  3894  iuncom4  3895  iunconstm  3896  iuniin  3898  iunss1  3899  ss2iun  3903  dfiun2g  3920  ssiun  3930  ssiun2  3931  iunab  3935  iun0  3945  0iun  3946  iunn0m  3949  iunin2  3952  iundif2ss  3954  iindif2m  3956  iunxsng  3964  iunxsngf  3966  iunun  3967  iunxun  3968  iunxiun  3970  iunpwss  3980  disjiun  4000  triun  4116  iunpw  4482  xpiundi  4686  xpiundir  4687  iunxpf  4777  cnvuni  4815  dmiun  4838  dmuni  4839  rniun  5041  dfco2  5130  dfco2a  5131  coiun  5140  fun11iun  5484  imaiun  5764  eluniimadm  5769  opabex3d  6125  opabex3  6126  smoiun  6305  tfrlemi14d  6337  tfr1onlemres  6353  tfrcllemres  6366  fsum2dlemstep  11445  fisumcom2  11449  fsumiun  11488  fprod2dlemstep  11633  fprodcom2fi  11637  ennnfonelemrn  12423  ennnfonelemdm  12424  ctiunctlemf  12442  ctiunctlemfo  12443  imasaddfnlemg  12741  lssats2  13539
  Copyright terms: Public domain W3C validator