Theorem eliun 3997

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 2827	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 2827	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 2658	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2297	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 2545	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 3995	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 2966	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 712	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1398   ∈ wcel 2205  ∃wrex 2523  Vcvv 2815  ∪ ciun 3993

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-iun 3995

This theorem is referenced by:  iuncom  3999  iuncom4  4000  iunconstm  4001  iuniin  4003  iunss1  4004  ss2iun  4008  dfiun2g  4025  ssiun  4035  ssiun2  4036  iunab  4040  iun0  4050  0iun  4051  iunn0m  4054  iunin2  4057  iundif2ss  4059  iindif2m  4061  iunxsng  4069  iunxsngf  4071  iunun  4072  iunxun  4073  iunxiun  4075  iunpwss  4085  disjiun  4106  triun  4223  iunpw  4603  xpiundi  4810  xpiundir  4811  iunxpf  4905  cnvuni  4943  dmiun  4967  dmuni  4968  rniun  5175  dfco2  5264  dfco2a  5265  coiun  5274  fun11iun  5637  imaiun  5935  eluniimadm  5940  opabex3d  6316  opabex3  6317  smoiun  6534  tfrlemi14d  6566  tfr1onlemres  6582  tfrcllemres  6595  wrdval  11235  fsum2dlemstep  12128  fisumcom2  12132  fsumiun  12171  fprod2dlemstep  12316  fprodcom2fi  12320  ennnfonelemrn  13191  ennnfonelemdm  13192  ctiunctlemf  13210  ctiunctlemfo  13211  imasaddfnlemg  13548  lssats2  14611  clwwlknun  16485