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 } |
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 } |