Metamath Proof Explorer


Theorem elrnmpores

Description: Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypothesis rngop.1 F = x A , y B C
Assertion elrnmpores D V D ran F R x A y B D = C x R y

Proof

Step Hyp Ref Expression
1 rngop.1 F = x A , y B C
2 eqeq1 z = D z = C D = C
3 2 anbi1d z = D z = C x R y D = C x R y
4 3 anbi2d z = D x A y B z = C x R y x A y B D = C x R y
5 4 2exbidv z = D x y x A y B z = C x R y x y x A y B D = C x R y
6 an12 p R p = x y x A y B z = C p = x y p R x A y B z = C
7 an12 p R x A y B z = C x A y B p R z = C
8 ancom z = C p R p R z = C
9 eleq1 p = x y p R x y R
10 df-br x R y x y R
11 9 10 bitr4di p = x y p R x R y
12 11 anbi2d p = x y z = C p R z = C x R y
13 8 12 bitr3id p = x y p R z = C z = C x R y
14 13 anbi2d p = x y x A y B p R z = C x A y B z = C x R y
15 7 14 syl5bb p = x y p R x A y B z = C x A y B z = C x R y
16 15 pm5.32i p = x y p R x A y B z = C p = x y x A y B z = C x R y
17 6 16 bitri p R p = x y x A y B z = C p = x y x A y B z = C x R y
18 17 2exbii x y p R p = x y x A y B z = C x y p = x y x A y B z = C x R y
19 19.42vv x y p R p = x y x A y B z = C p R x y p = x y x A y B z = C
20 18 19 bitr3i x y p = x y x A y B z = C x R y p R x y p = x y x A y B z = C
21 20 opabbii p z | x y p = x y x A y B z = C x R y = p z | p R x y p = x y x A y B z = C
22 dfoprab2 x y z | x A y B z = C x R y = p z | x y p = x y x A y B z = C x R y
23 df-mpo x A , y B C = x y z | x A y B z = C
24 dfoprab2 x y z | x A y B z = C = p z | x y p = x y x A y B z = C
25 1 23 24 3eqtri F = p z | x y p = x y x A y B z = C
26 25 reseq1i F R = p z | x y p = x y x A y B z = C R
27 resopab p z | x y p = x y x A y B z = C R = p z | p R x y p = x y x A y B z = C
28 26 27 eqtri F R = p z | p R x y p = x y x A y B z = C
29 21 22 28 3eqtr4ri F R = x y z | x A y B z = C x R y
30 29 rneqi ran F R = ran x y z | x A y B z = C x R y
31 rnoprab ran x y z | x A y B z = C x R y = z | x y x A y B z = C x R y
32 30 31 eqtri ran F R = z | x y x A y B z = C x R y
33 5 32 elab2g D V D ran F R x y x A y B D = C x R y
34 r2ex x A y B D = C x R y x y x A y B D = C x R y
35 33 34 bitr4di D V D ran F R x A y B D = C x R y