Metamath Proof Explorer


Theorem rnoprab2

Description: The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012)

Ref Expression
Assertion rnoprab2
|- ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } = { z | E. x e. A E. y e. B ph }

Proof

Step Hyp Ref Expression
1 rnoprab
 |-  ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) }
2 r2ex
 |-  ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
3 2 abbii
 |-  { z | E. x e. A E. y e. B ph } = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) }
4 1 3 eqtr4i
 |-  ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } = { z | E. x e. A E. y e. B ph }