Theorem eliun 3994

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 2824	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2824	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2656	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2295	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2543	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3992	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2963	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 712	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2203  ∃wrex 2521  Vcvv 2812  ∪ ciun 3990

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-iun 3992

This theorem is referenced by:  iuncom  3996  iuncom4  3997  iunconstm  3998  iuniin  4000  iunss1  4001  ss2iun  4005  dfiun2g  4022  ssiun  4032  ssiun2  4033  iunab  4037  iun0  4047  0iun  4048  iunn0m  4051  iunin2  4054  iundif2ss  4056  iindif2m  4058  iunxsng  4066  iunxsngf  4068  iunun  4069  iunxun  4070  iunxiun  4072  iunpwss  4082  disjiun  4103  triun  4220  iunpw  4600  xpiundi  4807  xpiundir  4808  iunxpf  4902  cnvuni  4940  dmiun  4964  dmuni  4965  rniun  5172  dfco2  5261  dfco2a  5262  coiun  5271  fun11iun  5634  imaiun  5932  eluniimadm  5937  opabex3d  6313  opabex3  6314  smoiun  6531  tfrlemi14d  6563  tfr1onlemres  6579  tfrcllemres  6592  wrdval  11220  fsum2dlemstep  12113  fisumcom2  12117  fsumiun  12156  fprod2dlemstep  12301  fprodcom2fi  12305  ennnfonelemrn  13159  ennnfonelemdm  13160  ctiunctlemf  13178  ctiunctlemfo  13179  imasaddfnlemg  13516  lssats2  14549  clwwlknun  16423