Metamath Proof Explorer


Theorem fnoprab

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 }

Proof

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 }