Theorem hbxfr 1992

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 1961	. 2 |- (y e. A <-> y e. B)
4	3	albii 1346	. 2 |- (A.x y e. A <-> A.x y e. B)
5	1, 3, 4	3imtr4i 236	1 |- (y e. A -> A.x y e. A)

Syntax hints:   -> wi 3  A.wal 1296   = wceq 1298   e. wcel 1300

This theorem is referenced by:  hbrab1 2257  hbrab 2258  hbif 2999  hbifOLD 3000  hbsn 3088  hbop 3168  hbeqel 3195  hbiu1 3281  hbii1 3282  hbopab 3560  hbopab1 3562  hbopab2 3563  hbxp 4024  hbco 4129  hbdm 4200  hbres 4220  hbima 4273  fnopabg 4546  hbfv 4686  fvopab5 4756  elrnopabg 4773  rnssopab 4798  fopabco 4805  hbopr 4904  hboprab1 4919  hboprab2 4920  hbmpt1 5010  elrnoprabg 5066  hbiota1 5091  hbiota 5092  hbrdg 5144  abianfplem 5170  hbriota1 5569  hbriota 5570  xpmapenlem1 5590  xpmapenlem4 5593  trcl 5752  tz9.12lem3 5772  hta 5858  ac6lem 5916  alephfplem2 6045  hbneg 6517  om2uzsuci 7707  hbsum1 8243  hbsum 8244  fsumserz2 8263  serzfsum 8264  isumval2 8455  isumclim4 8462  isumcmpii 8476  minvecdist 9930  cnlnadjlem5 11641  bnj898 12815  bnj1230 13002  bnj1317 13053  bnj1441 13134  bnj900 13325  bnj958 13344  bnj965 13346  bnj1000 13364  bnj1014 13374  bnj1123 13422  bnj1145 13431  bnj1137 13433  bnj1309 13487  bnj1307 13488  bnj1398 13515  bnj1404 13517  bnj1443 13533  bnj1444 13534  bnj1445 13535  bnj1446 13536  bnj1447 13537  bnj1448 13538  bnj1449 13539  bnj1466 13548  bnj1467 13549  bnj1499 13561  bnj1518 13567  bnj1519 13568  bnj1520 13569  bnj1525 13572  bnj1535 13576  hbprod1 14659  hbprod 14660  fnopabco2b 14734  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  hbstr1 16710  hbstb1 16727  stbval 16731  stb2xpl 16742  stb3xpl 16743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain