Theorem eluni 2510

Description: Membership in class union.

Assertion

Ref	Expression
eluni	|- (A e. U.B <-> E.x(A e. x /\ x e. B))

Distinct variable groups:   x,A   x,B

Proof of Theorem eluni

Step	Hyp	Ref	Expression
1		elisset 1820	. 2 |- (A e. U.B -> A e. V)
2		elisset 1820	. . . 4 |- (A e. x -> A e. V)
3	2	adantr 391	. . 3 |- ((A e. x /\ x e. B) -> A e. V)
4	3	19.23aiv 1297	. 2 |- (E.x(A e. x /\ x e. B) -> A e. V)
5		eleq1 1537	. . . . 5 |- (y = A -> (y e. x <-> A e. x))
6	5	anbi1d 619	. . . 4 |- (y = A -> ((y e. x /\ x e. B) <-> (A e. x /\ x e. B)))
7	6	exbidv 1281	. . 3 |- (y = A -> (E.x(y e. x /\ x e. B) <-> E.x(A e. x /\ x e. B)))
8		df-uni 2508	. . 3 |- U.B = {y | E.x(y e. x /\ x e. B)}
9	7, 8	elab2g 1903	. 2 |- (A e. V -> (A e. U.B <-> E.x(A e. x /\ x e. B)))
10	1, 4, 9	pm5.21nii 681	1 |- (A e. U.B <-> E.x(A e. x /\ x e. B))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  Vcvv 1814  U.cuni 2507

This theorem is referenced by:  eluni2 2511  elunii 2512  hbuni 2513  eluniab 2517  uniun 2523  uniin 2524  ssuni 2526  unissb 2532  iununi 2621  dftr2 2687  unipw 2762  uniex2 2875  uniuni 2886  dmuni 3325  rnuni 3465  fununi 3569  imaiun 3870  funiunfv 3872  elunirnALT 3875  tfrlem7 3923  uniixp 4363  inf2 4617  inf3lem2 4623  kmlem3 4777  kmlem4 4778  unidom 4818  carduni 4869  cfub 4920  suplem1pr 5173  isbasis2g 7611  tgval2t 7616  tgss3t 7637  basgent 7639  uninqs 10436

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-uni 2508

Copyright terms: Public domain