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 ranxyz|xAyBφ=z|xAyBφ

Proof

Step Hyp Ref Expression
1 rnoprab ranxyz|xAyBφ=z|xyxAyBφ
2 r2ex xAyBφxyxAyBφ
3 2 abbii z|xAyBφ=z|xyxAyBφ
4 1 3 eqtr4i ranxyz|xAyBφ=z|xAyBφ