Metamath Proof Explorer


Theorem elovmporab1w

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Version of elovmporab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses elovmporab1w.o O=xV,yVzx/mM|φ
elovmporab1w.v XVYVX/mMV
Assertion elovmporab1w ZXOYXVYVZX/mM

Proof

Step Hyp Ref Expression
1 elovmporab1w.o O=xV,yVzx/mM|φ
2 elovmporab1w.v XVYVX/mMV
3 1 elmpocl ZXOYXVYV
4 1 a1i XVYVO=xV,yVzx/mM|φ
5 csbeq1 x=Xx/mM=X/mM
6 5 ad2antrl XVYVx=Xy=Yx/mM=X/mM
7 sbceq1a y=Yφ[˙Y/y]˙φ
8 sbceq1a x=X[˙Y/y]˙φ[˙X/x]˙[˙Y/y]˙φ
9 7 8 sylan9bbr x=Xy=Yφ[˙X/x]˙[˙Y/y]˙φ
10 9 adantl XVYVx=Xy=Yφ[˙X/x]˙[˙Y/y]˙φ
11 6 10 rabeqbidv XVYVx=Xy=Yzx/mM|φ=zX/mM|[˙X/x]˙[˙Y/y]˙φ
12 eqidd XVYVx=XV=V
13 simpl XVYVXV
14 simpr XVYVYV
15 rabexg X/mMVzX/mM|[˙X/x]˙[˙Y/y]˙φV
16 2 15 syl XVYVzX/mM|[˙X/x]˙[˙Y/y]˙φV
17 nfcv _xX
18 17 nfel1 xXV
19 nfcv _xY
20 19 nfel1 xYV
21 18 20 nfan xXVYV
22 nfcv _yX
23 22 nfel1 yXV
24 nfcv _yY
25 24 nfel1 yYV
26 23 25 nfan yXVYV
27 nfsbc1v x[˙X/x]˙[˙Y/y]˙φ
28 nfcv _xM
29 17 28 nfcsbw _xX/mM
30 27 29 nfrabw _xzX/mM|[˙X/x]˙[˙Y/y]˙φ
31 nfsbc1v y[˙Y/y]˙φ
32 22 31 nfsbcw y[˙X/x]˙[˙Y/y]˙φ
33 nfcv _yM
34 22 33 nfcsbw _yX/mM
35 32 34 nfrabw _yzX/mM|[˙X/x]˙[˙Y/y]˙φ
36 4 11 12 13 14 16 21 26 22 19 30 35 ovmpodxf XVYVXOY=zX/mM|[˙X/x]˙[˙Y/y]˙φ
37 36 eleq2d XVYVZXOYZzX/mM|[˙X/x]˙[˙Y/y]˙φ
38 df-3an XVYVZX/mMXVYVZX/mM
39 38 simplbi2com ZX/mMXVYVXVYVZX/mM
40 elrabi ZzX/mM|[˙X/x]˙[˙Y/y]˙φZX/mM
41 39 40 syl11 XVYVZzX/mM|[˙X/x]˙[˙Y/y]˙φXVYVZX/mM
42 37 41 sylbid XVYVZXOYXVYVZX/mM
43 3 42 mpcom ZXOYXVYVZX/mM