Metamath Proof Explorer

Theorem ovmpodv2

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Hypotheses ovmpodv2.1 
|- ( ph -> A e. C )
ovmpodv2.2 
|- ( ( ph /\ x = A ) -> B e. D )
ovmpodv2.3 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )
ovmpodv2.4 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
Assertion ovmpodv2 
|- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = S ) )

Proof

Step Hyp Ref Expression
1 ovmpodv2.1 
 |-  ( ph -> A e. C )
2 ovmpodv2.2 
 |-  ( ( ph /\ x = A ) -> B e. D )
3 ovmpodv2.3 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )
4 ovmpodv2.4 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )
5 eqidd 
 |-  ( ph -> ( x e. C , y e. D |-> R ) = ( x e. C , y e. D |-> R ) )
6 4 eqeq2d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A ( x e. C , y e. D |-> R ) B ) = R <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
7 6 biimpd 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A ( x e. C , y e. D |-> R ) B ) = R -> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
8 nfmpo1 
 |-  F/_ x ( x e. C , y e. D |-> R )
9 nfcv 
 |-  F/_ x A
10 nfcv 
 |-  F/_ x B
11 9 8 10 nfov 
 |-  F/_ x ( A ( x e. C , y e. D |-> R ) B )
12 11 nfeq1 
 |-  F/ x ( A ( x e. C , y e. D |-> R ) B ) = S
13 nfmpo2 
 |-  F/_ y ( x e. C , y e. D |-> R )
14 nfcv 
 |-  F/_ y A
15 nfcv 
 |-  F/_ y B
16 14 13 15 nfov 
 |-  F/_ y ( A ( x e. C , y e. D |-> R ) B )
17 16 nfeq1 
 |-  F/ y ( A ( x e. C , y e. D |-> R ) B ) = S
18 1 2 3 7 8 12 13 17 ovmpodf 
 |-  ( ph -> ( ( x e. C , y e. D |-> R ) = ( x e. C , y e. D |-> R ) -> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
19 5 18 mpd 
 |-  ( ph -> ( A ( x e. C , y e. D |-> R ) B ) = S )
20 oveq 
 |-  ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = ( A ( x e. C , y e. D |-> R ) B ) )
21 20 eqeq1d 
 |-  ( F = ( x e. C , y e. D |-> R ) -> ( ( A F B ) = S <-> ( A ( x e. C , y e. D |-> R ) B ) = S ) )
22 19 21 syl5ibrcom 
 |-  ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = S ) )