Metamath Proof Explorer

Theorem elovmpoeq

Description: If a value of an operation given by maps-to notation has a member, it equals the substituted body. (Contributed by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses elovmpoeq.f 
|- F = ( x e. A , y e. B |-> C )
elovmpoeq.s 
|- ( ( x = X /\ y = Y ) -> C = D )
Assertion elovmpoeq 
|- ( N e. ( X F Y ) -> ( X F Y ) = D )

Proof

Step Hyp Ref Expression
1 elovmpoeq.f 
 |-  F = ( x e. A , y e. B |-> C )
2 elovmpoeq.s 
 |-  ( ( x = X /\ y = Y ) -> C = D )
3 ne0i 
 |-  ( N e. ( X F Y ) -> ( X F Y ) =/= (/) )
4 df-ov 
 |-  ( X F Y ) = ( F ` <. X , Y >. )
5 4 eqcomi 
 |-  ( F ` <. X , Y >. ) = ( X F Y )
6 tz6.12i 
 |-  ( ( X F Y ) =/= (/) -> ( ( F ` <. X , Y >. ) = ( X F Y ) -> <. X , Y >. F ( X F Y ) ) )
7 3 5 6 mpisyl 
 |-  ( N e. ( X F Y ) -> <. X , Y >. F ( X F Y ) )
8 df-br 
 |-  ( <. X , Y >. F ( X F Y ) <-> <. <. X , Y >. , ( X F Y ) >. e. F )
9 7 8 sylib 
 |-  ( N e. ( X F Y ) -> <. <. X , Y >. , ( X F Y ) >. e. F )
10 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
11 1 10 eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
12 9 11 eleqtrdi 
 |-  ( N e. ( X F Y ) -> <. <. X , Y >. , ( X F Y ) >. e. { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } )
13 1 elmpocl1 
 |-  ( N e. ( X F Y ) -> X e. A )
14 13 elexd 
 |-  ( N e. ( X F Y ) -> X e. _V )
15 1 elmpocl2 
 |-  ( N e. ( X F Y ) -> Y e. B )
16 15 elexd 
 |-  ( N e. ( X F Y ) -> Y e. _V )
17 ovexd 
 |-  ( N e. ( X F Y ) -> ( X F Y ) e. _V )
18 simp1 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> x = X )
19 18 eleq1d 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> ( x e. A <-> X e. A ) )
20 simp2 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> y = Y )
21 20 eleq1d 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> ( y e. B <-> Y e. B ) )
22 19 21 anbi12d 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> ( ( x e. A /\ y e. B ) <-> ( X e. A /\ Y e. B ) ) )
23 simp3 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> z = ( X F Y ) )
24 2 3adant3 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> C = D )
25 23 24 eqeq12d 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> ( z = C <-> ( X F Y ) = D ) )
26 22 25 anbi12d 
 |-  ( ( x = X /\ y = Y /\ z = ( X F Y ) ) -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( X e. A /\ Y e. B ) /\ ( X F Y ) = D ) ) )
27 26 eloprabga 
 |-  ( ( X e. _V /\ Y e. _V /\ ( X F Y ) e. _V ) -> ( <. <. X , Y >. , ( X F Y ) >. e. { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } <-> ( ( X e. A /\ Y e. B ) /\ ( X F Y ) = D ) ) )
28 14 16 17 27 syl3anc 
 |-  ( N e. ( X F Y ) -> ( <. <. X , Y >. , ( X F Y ) >. e. { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } <-> ( ( X e. A /\ Y e. B ) /\ ( X F Y ) = D ) ) )
29 12 28 mpbid 
 |-  ( N e. ( X F Y ) -> ( ( X e. A /\ Y e. B ) /\ ( X F Y ) = D ) )
30 29 simprd 
 |-  ( N e. ( X F Y ) -> ( X F Y ) = D )