Theorem hbuni 2513

Description: Bound-variable hypothesis builder for union.

Hypothesis

Ref	Expression
hbuni.1	|- (y e. A -> A.x y e. A)

Assertion

Ref	Expression
hbuni	|- (y e. U.A -> A.x y e. U.A)

Distinct variable groups:   y,A   x,y

Proof of Theorem hbuni

Step	Hyp	Ref	Expression
1		ax-17 973	. . . 4 |- (y e. z -> A.x y e. z)
2		hbuni.1	. . . . 5 |- (y e. A -> A.x y e. A)
3	1, 2	hbel 1569	. . . 4 |- (z e. A -> A.x z e. A)
4	1, 3	hban 1011	. . 3 |- ((y e. z /\ z e. A) -> A.x(y e. z /\ z e. A))
5	4	hbex 1008	. 2 |- (E.z(y e. z /\ z e. A) -> A.xE.z(y e. z /\ z e. A))
6		eluni 2510	. 2 |- (y e. U.A <-> E.z(y e. z /\ z e. A))
7	6	albii 1001	. 2 |- (A.x y e. U.A <-> A.xE.z(y e. z /\ z e. A))
8	5, 6, 7	3imtr4 219	1 |- (y e. U.A -> A.x y e. U.A)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 956   e. wcel 960  E.wex 982  U.cuni 2507

This theorem is referenced by:  euuni 2887  reuuni2f 2889  reucl 2891  reuuni4 2893  reuuniss 2895  reuuniss2 2897  reuunixfr 2912  hbfv 3735  hbrdg 3942  trcl 4655  cardprc 4872  lble 6049  reuunineg 6068  hbsum1 6983  hbsum 6984  tgval3t 7624  minvecdist 8581  fgsb 10555  fgsb2 10560

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