Theorem abidhb 2423

Description: Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)

Assertion

Ref	Expression
abidhb	|- (A.y(y e. A -> A.x y e. A) -> {z | A.x z e. A} = A)

Distinct variable groups:   y,A   x,z   x,y   z,A

Proof of Theorem abidhb

Step	Hyp	Ref	Expression
1		hba1 1350	. . . 4 |- (A.y(y e. A -> A.x y e. A) -> A.yA.y(y e. A -> A.x y e. A))
2		ax4 1318	. . . . 5 |- (A.x y e. A -> y e. A)
3		ax4 1318	. . . . 5 |- (A.y(y e. A -> A.x y e. A) -> (y e. A -> A.x y e. A))
4	2, 3	impbid2 576	. . . 4 |- (A.y(y e. A -> A.x y e. A) -> (A.x y e. A <-> y e. A))
5	1, 4	abbid 2007	. . 3 |- (A.y(y e. A -> A.x y e. A) -> {y | A.x y e. A} = {y | y e. A})
6		eleq1 1957	. . . . 5 |- (y = w -> (y e. A <-> w e. A))
7	6	albidv 1656	. . . 4 |- (y = w -> (A.x y e. A <-> A.x w e. A))
8	7	cbvabv 2420	. . 3 |- {y | A.x y e. A} = {w | A.x w e. A}
9		abid2 2011	. . 3 |- {y | y e. A} = A
10	5, 8, 9	3eqtr3g 1952	. 2 |- (A.y(y e. A -> A.x y e. A) -> {w | A.x w e. A} = A)
11		ax-17 1317	. . 3 |- (A.x z e. A -> A.wA.x z e. A)
12		ax-17 1317	. . 3 |- (A.x w e. A -> A.zA.x w e. A)
13		eleq1 1957	. . . 4 |- (z = w -> (z e. A <-> w e. A))
14	13	albidv 1656	. . 3 |- (z = w -> (A.x z e. A <-> A.x w e. A))
15	11, 12, 14	cbvab 2419	. 2 |- {z | A.x z e. A} = {w | A.x w e. A}
16	10, 15	syl5eq 1940	1 |- (A.y(y e. A -> A.x y e. A) -> {z | A.x z e. A} = A)

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

This theorem is referenced by:  hbeqd 2424  hbeld 2425  dedhb 2426  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  hbopd 3169  hbbrdOLD 3383  hbimad 4275  hbfvd 4687  hbfvd2 4688  hboprdOLD 4906  hbnegdOLD 6519

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880

Copyright terms: Public domain