Theorem eluni 1922

Description: Membership in class union.

Assertion

Ref	Expression
eluni	⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B))

Distinct variable group(s):   x,A   x,B

Proof of Theorem eluni

Step	Hyp	Ref	Expression
1		elisset 1354	. 2 ⊢ (A ∈ ∪B → A ∈ V)
2		elisset 1354	. . . 4 ⊢ (A ∈ x → A ∈ V)
3	2	adantr 306	. . 3 ⊢ ((A ∈ x ∧ x ∈ B) → A ∈ V)
4	3	19.23aiv 952	. 2 ⊢ (∃x(A ∈ x ∧ x ∈ B) → A ∈ V)
5		eleq1 1149	. . . . 5 ⊢ (y = A → (y ∈ x ↔ A ∈ x))
6	5	anbi1d 469	. . . 4 ⊢ (y = A → ((y ∈ x ∧ x ∈ B) ↔ (A ∈ x ∧ x ∈ B)))
7	6	biexdv 936	. . 3 ⊢ (y = A → (∃x(y ∈ x ∧ x ∈ B) ↔ ∃x(A ∈ x ∧ x ∈ B)))
8		df-uni 1920	. . 3 ⊢ ∪B = {y∣∃x(y ∈ x ∧ x ∈ B)}
9	7, 8	elab2g 1418	. 2 ⊢ (A ∈ V → (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B)))
10	1, 4, 9	pm5.21nii 504	1 ⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092  Vcvv 1348  ∪cuni 1919

This theorem is referenced by:  eluni2 1923  elunii 1924  hbuni 1925  eluniab 1926  uniun 1934  uniin 1935  ssuni 1937  unissb 1941  uniex 1947  unipw 1960  iununi 2037  dftr2 2043  dmuni 2538  rnuni 2646  imaiun 2650  fununi 2705  tfrlem7 2955  inf2 3459  inf3lem2 3465  kmlem3 3582  kmlem4 3583  carduni 3664  cfub 3703  suplem1pr 3955

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-uni 1920

metamath.org