Theorem eluni 2501

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 1813	. 2 |- (A e. U.B -> A e. V)
2		elisset 1813	. . . 4 |- (A e. x -> A e. V)
3	2	adantr 389	. . 3 |- ((A e. x /\ x e. B) -> A e. V)
4	3	19.23aiv 1293	. 2 |- (E.x(A e. x /\ x e. B) -> A e. V)
5		eleq1 1531	. . . . 5 |- (y = A -> (y e. x <-> A e. x))
6	5	anbi1d 616	. . . 4 |- (y = A -> ((y e. x /\ x e. B) <-> (A e. x /\ x e. B)))
7	6	exbidv 1277	. . 3 |- (y = A -> (E.x(y e. x /\ x e. B) <-> E.x(A e. x /\ x e. B)))
8		df-uni 2499	. . 3 |- U.B = {y | E.x(y e. x /\ x e. B)}
9	7, 8	elab2g 1896	. 2 |- (A e. V -> (A e. U.B <-> E.x(A e. x /\ x e. B)))
10	1, 4, 9	pm5.21nii 678	1 |- (A e. U.B <-> E.x(A e. x /\ x e. B))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 954   e. wcel 956  E.wex 978  Vcvv 1807  U.cuni 2498

This theorem is referenced by:  eluni2 2502  elunii 2503  hbuni 2504  eluniab 2508  uniun 2514  uniin 2515  ssuni 2517  unissb 2523  iununi 2611  dftr2 2677  unipw 2751  uniex2 2864  uniuni 2875  dmuni 3314  rnuni 3451  fununi 3555  imaiun 3855  funiunfv 3857  elunirnALT 3860  tfrlem7 3908  uniixp 4347  inf2 4588  inf3lem2 4594  kmlem3 4747  kmlem4 4748  unidom 4788  carduni 4838  cfub 4888  suplem1pr 5141  isbasis2g 7562  tgval2t 7567  tgss3t 7588  basgent 7590  uninqs 10378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-uni 2499

Copyright terms: Public domain