Theorem hbuni 2504

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 969	. . . 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 1563	. . . 4 |- (z e. A -> A.x z e. A)
4	1, 3	hban 1007	. . 3 |- ((y e. z /\ z e. A) -> A.x(y e. z /\ z e. A))
5	4	hbex 1004	. 2 |- (E.z(y e. z /\ z e. A) -> A.xE.z(y e. z /\ z e. A))
6		eluni 2501	. 2 |- (y e. U.A <-> E.z(y e. z /\ z e. A))
7	6	albii 997	. 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 952   e. wcel 956  E.wex 978  U.cuni 2498

This theorem is referenced by:  euuni 2876  reuuni2f 2878  reucl 2880  reuuni4 2882  reuuniss 2884  reuuniss2 2886  reuunixfr 2901  hbfv 3720  hbrdg 3927  trcl 4625  cardprc 4841  lble 6002  reuunineg 6021  hbsum1 6929  hbsum 6930  tgval3t 7575  minvecdist 8529  fgsb 10480  fgsb2 10485

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