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

Theorem eliun 3877
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 2741 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 2741 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 2583 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2233 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 2471 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 3875 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 2877 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 699 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1348  wcel 2141  wrex 2449  Vcvv 2730   ciun 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-iun 3875
This theorem is referenced by:  iuncom  3879  iuncom4  3880  iunconstm  3881  iuniin  3883  iunss1  3884  ss2iun  3888  dfiun2g  3905  ssiun  3915  ssiun2  3916  iunab  3919  iun0  3929  0iun  3930  iunn0m  3933  iunin2  3936  iundif2ss  3938  iindif2m  3940  iunxsng  3948  iunxsngf  3950  iunun  3951  iunxun  3952  iunxiun  3954  iunpwss  3964  disjiun  3984  triun  4100  iunpw  4465  xpiundi  4669  xpiundir  4670  iunxpf  4759  cnvuni  4797  dmiun  4820  dmuni  4821  rniun  5021  dfco2  5110  dfco2a  5111  coiun  5120  fun11iun  5463  imaiun  5739  eluniimadm  5744  opabex3d  6100  opabex3  6101  smoiun  6280  tfrlemi14d  6312  tfr1onlemres  6328  tfrcllemres  6341  fsum2dlemstep  11397  fisumcom2  11401  fsumiun  11440  fprod2dlemstep  11585  fprodcom2fi  11589  ennnfonelemrn  12374  ennnfonelemdm  12375  ctiunctlemf  12393  ctiunctlemfo  12394
  Copyright terms: Public domain W3C validator