Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fnoprab.1 | |- ( ph -> E! z ps ) |
|
Assertion | fnoprab | |- { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnoprab.1 | |- ( ph -> E! z ps ) |
|
2 | 1 | gen2 | |- A. x A. y ( ph -> E! z ps ) |
3 | fnoprabg | |- ( A. x A. y ( ph -> E! z ps ) -> { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } ) |
|
4 | 2 3 | ax-mp | |- { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } |