Theorem eliun 3948

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.

Step	Hyp	Ref	Expression
1		elex 2791	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2791	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2624	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2272	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2511	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3946	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2930	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 708	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1375   ∈ wcel 2180  ∃wrex 2489  Vcvv 2779  ∪ ciun 3944

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-iun 3946

This theorem is referenced by:  iuncom  3950  iuncom4  3951  iunconstm  3952  iuniin  3954  iunss1  3955  ss2iun  3959  dfiun2g  3976  ssiun  3986  ssiun2  3987  iunab  3991  iun0  4001  0iun  4002  iunn0m  4005  iunin2  4008  iundif2ss  4010  iindif2m  4012  iunxsng  4020  iunxsngf  4022  iunun  4023  iunxun  4024  iunxiun  4026  iunpwss  4036  disjiun  4057  triun  4174  iunpw  4548  xpiundi  4754  xpiundir  4755  iunxpf  4847  cnvuni  4885  dmiun  4909  dmuni  4910  rniun  5115  dfco2  5204  dfco2a  5205  coiun  5214  fun11iun  5569  imaiun  5857  eluniimadm  5862  opabex3d  6236  opabex3  6237  smoiun  6417  tfrlemi14d  6449  tfr1onlemres  6465  tfrcllemres  6478  wrdval  11041  fsum2dlemstep  11911  fisumcom2  11915  fsumiun  11954  fprod2dlemstep  12099  fprodcom2fi  12103  ennnfonelemrn  12956  ennnfonelemdm  12957  ctiunctlemf  12975  ctiunctlemfo  12976  imasaddfnlemg  13313  lssats2  14343