Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfopab.1 | |- F/ z ph |
|
Assertion | nfopab | |- F/_ z { <. x , y >. | ph } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfopab.1 | |- F/ z ph |
|
2 | df-opab | |- { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) } |
|
3 | nfv | |- F/ z w = <. x , y >. |
|
4 | 3 1 | nfan | |- F/ z ( w = <. x , y >. /\ ph ) |
5 | 4 | nfex | |- F/ z E. y ( w = <. x , y >. /\ ph ) |
6 | 5 | nfex | |- F/ z E. x E. y ( w = <. x , y >. /\ ph ) |
7 | 6 | nfab | |- F/_ z { w | E. x E. y ( w = <. x , y >. /\ ph ) } |
8 | 2 7 | nfcxfr | |- F/_ z { <. x , y >. | ph } |