Theorem hbxfr 1566

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 1541	. 2 |- (y e. A <-> y e. B)
4	3	albii 1001	. 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 956   = wceq 958   e. wcel 960

This theorem is referenced by:  hbrab1 1775  hbrab 1776  hbif 2377  hbsn 2442  hbop 2500  hbiu1 2588  hbii1 2589  hbopab1 2819  hbopab2 2820  hbco 3293  hbdm 3358  hbres 3376  fnopabg 3621  hbfv 3735  fvopab5 3799  elrnopabg 3806  rnssopab 3831  fopabco 3838  hbrdg 3942  abianfplem 3967  hbopr 3987  hboprab1 3999  hboprab2 4000  elrnoprabg 4130  xpmapenlem1 4502  xpmapenlem4 4505  trcl 4655  tz9.12lem3 4671  hta 4738  ac6lem 4764  alephfplem2 4908  hbneg 5374  om2uzsuc 6297  hbsum1 6983  hbsum 6984  fsumserz2 7003  serzfsum 7004  isumval2t 7194  isumclim4t 7201  isumcmpi 7215  minvecdist 8581  cnlnadjlem5 9999  hbcmpt 10452

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475

Copyright terms: Public domain