HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem hbab 1460
Description: Bound-variable hypothesis builder for a class abstraction.
Hypothesis
Ref Expression
hbab.1 |- (ph -> A.xph)
Assertion
Ref Expression
hbab |- (z e. {y | ph} -> A.x z e. {y | ph})
Distinct variable group:   x,z

Proof of Theorem hbab
StepHypRef Expression
1 ax-16 1206 . . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2 hbab.1 . . . 4 |- (ph -> A.xph)
32hbsb4 1243 . . 3 |- (-. A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
41, 3pm2.61i 126 . 2 |- ([z / y]ph -> A.x[z / y]ph)
5 df-clab 1457 . 2 |- (z e. {y | ph} <-> [z / y]ph)
65albii 996 . 2 |- (A.x z e. {y | ph} <-> A.x[z / y]ph)
74, 5, 63imtr4 219 1 |- (z e. {y | ph} -> A.x z e. {y | ph})
Colors of variables: wff set class
Syntax hints:   -> wi 3  A.wal 951   = wceq 953   e. wcel 955  [wsbc 1166  {cab 1456
This theorem is referenced by:  hbrab 1765  cbvab 1899  hbeqd 1904  hbeld 1905  hbsbc1gd 1973  hbsbcgd 1974  hbif 2363  hbopd 2488  intab 2550  hbiu1 2574  hbii1 2575  hbbrd 2649  moop2 2790  hbopab1 2802  hbopab2 2803  hbimad 3396  hbfv 3714  hbfvd 3715  hbfvd2 3716  fvopabgf 3772  fvopabnf 3773  hbrdg 3921  hboprd 3967  hboprab1 3978  hboprab2 3979  oprabval4g 4016  hta 4700  hbnegd 5335  seq1lem1 6246  hbsum1 6921  hbsum 6922  fsum1f 6945  fsump1f 6949
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457
Copyright terms: Public domain