Theorem eluni 3916

Description: Membership in class union. (Contributed by NM, 22-May-1994.)

Assertion

Ref	Expression
eluni	⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2824	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 → 𝐴 ∈ V)
2		elex 2824	. . . 4 ⊢ (𝐴 ∈ 𝑥 → 𝐴 ∈ V)
3	2	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
4	3	exlimiv 1647	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ V)
5		eleq1 2295	. . . . 5 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
6	5	anbi1d 465	. . . 4 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
7	6	exbidv 1874	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
8		df-uni 3914	. . 3 ⊢ ∪ 𝐵 = {𝑦 ∣ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)}
9	7, 8	elab2g 2963	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)))
10	1, 4, 9	pm5.21nii 712	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2203  Vcvv 2812  ∪ cuni 3913

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-v 2814  df-uni 3914

This theorem is referenced by:  eluni2  3917  elunii  3918  eluniab  3925  uniun  3932  uniin  3933  uniss  3934  unissb  3943  dftr2  4209  unidif0  4279  unipw  4332  uniex2  4556  uniuni  4571  limom  4735  dmuni  4965  fununi  5423  nfvres  5705  elunirn  5938  tfrlem7  6547  tfrexlem  6564  tfrcldm  6593  fiuni  7264  isbasis2g  14902  tgval2  14908  ntreq0  14989  bj-uniex2  16678