Theorem hbbr 2654

Description: Bound-variable hypothesis builder for binary relation.

Hypotheses

Ref	Expression
hbbr.1	|- (y e. A -> A.x y e. A)
hbbr.2	|- (y e. R -> A.x y e. R)
hbbr.3	|- (y e. B -> A.x y e. B)

Assertion

Ref	Expression
hbbr	|- (ARB -> A.x ARB)

Distinct variable groups:   y,A   y,B   y,R   x,y

Proof of Theorem hbbr

Step	Hyp	Ref	Expression
1		hbbr.1	. . . 4 |- (y e. A -> A.x y e. A)
2		hbbr.3	. . . 4 |- (y e. B -> A.x y e. B)
3	1, 2	hbop 2493	. . 3 |- (y e. <.A, B>. -> A.x y e. <.A, B>.)
4		hbbr.2	. . 3 |- (y e. R -> A.x y e. R)
5	3, 4	hbel 1564	. 2 |- (<.A, B>. e. R -> A.x<.A, B>. e. R)
6		df-br 2616	. 2 |- (ARB <-> <.A, B>. e. R)
7	6	albii 998	. 2 |- (A.x ARB <-> A.x<.A, B>. e. R)
8	5, 6, 7	3imtr4 219	1 |- (ARB -> A.x ARB)

Syntax hints:   -> wi 3  A.wal 953   e. wcel 957  <.cop 2408   class class class wbr 2615

This theorem is referenced by:  hbbrd 2655  sbcbrg 2658  hbco 3283  hbcnv 3291  dffunmof 3526  funfv2f 3767  hbiso 3887  uniimadomf 4794  ondomcard 4840  cardmin 4843  alephordlem1 4855  lble 6004  hbsum1 6936  hbsum 6937  isumcmpi 7167  irredt 10278

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616

Copyright terms: Public domain