Theorem eluni2 2502

Description: Membership in class union. Restricted quantifier version.

Assertion

Ref	Expression
eluni2	|- (A e. U.B <-> E.x e. B A e. x)

Distinct variable groups:   x,A   x,B

Proof of Theorem eluni2

Step	Hyp	Ref	Expression
1		exancom 1052	. 2 |- (E.x(A e. x /\ x e. B) <-> E.x(x e. B /\ A e. x))
2		eluni 2501	. 2 |- (A e. U.B <-> E.x(A e. x /\ x e. B))
3		df-rex 1647	. 2 |- (E.x e. B A e. x <-> E.x(x e. B /\ A e. x))
4	1, 2, 3	3bitr4 183	1 |- (A e. U.B <-> E.x e. B A e. x)

Syntax hints:   <-> wb 146   /\ wa 223   e. wcel 956  E.wex 978  E.wrex 1643  U.cuni 2498

This theorem is referenced by:  uni0b 2518  intssuni 2550  iununi 2611  ssorduni 2988  unon 3083  limuni3 3118  reluni 3260  cnvuni 3296  chfnrn 3793  rankuni2 4670  cflim 4889  isbasis3g 7563  unitgt 7573  tgclt 7574  basgen2t 7589  bastop 7592  opnuni 7820  unirnbl 7827  axgroth3 8718  ntunte 10376

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-rex 1647  df-v 1808  df-uni 2499

Copyright terms: Public domain