Theorem hbxfr 1561

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition.

Hypotheses

Ref	Expression
hbxfr.1	|- A = B
hbxfr.2	|- (y e. B -> A.x y e. B)

Assertion

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

Proof of Theorem hbxfr

Step	Hyp	Ref	Expression
1		hbxfr.2	. 2 |- (y e. B -> A.x y e. B)
2		hbxfr.1	. . 3 |- A = B
3	2	eleq2i 1536	. 2 |- (y e. A <-> y e. B)
4	3	albii 998	. 2 |- (A.x y e. A <-> A.x y e. B)
5	1, 3, 4	3imtr4 219	1 |- (y e. A -> A.x y e. A)

Syntax hints:   -> wi 3  A.wal 953   = wceq 955   e. wcel 957

This theorem is referenced by:  hbrab1 1770  hbrab 1771  hbif 2370  hbsn 2435  hbop 2493  hbiu1 2580  hbii1 2581  hbopab1 2809  hbopab2 2810  hbco 3283  hbdm 3348  hbres 3366  fnopabg 3611  hbfv 3724  fvopab5 3788  elrnopabg 3795  rnssopab 3820  fopabco 3827  hbrdg 3931  abianfplem 3956  hbopr 3976  hboprab1 3988  hboprab2 3989  elrnoprabg 4117  xpmapenlem1 4485  xpmapenlem4 4488  trcl 4628  tz9.12lem3 4644  hta 4711  ac6lem 4737  alephfplem2 4880  hbneg 5345  om2uzsuc 6246  hbsum1 6936  hbsum 6937  fsumserz2 6956  serzfsum 6957  isumval2t 7147  isumclim4t 7153  isumcmpi 7167  minvecdist 8544  cnlnadjlem5 9960  hbcmpt 10416

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1468  df-clel 1471

Copyright terms: Public domain