This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvmpo1

Description: Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses cbvmpo1.1 
|- F/_ x B
cbvmpo1.2 
|- F/_ z B
cbvmpo1.3 
|- F/_ z C
cbvmpo1.4 
|- F/_ x E
cbvmpo1.5 
|- ( x = z -> C = E )
Assertion cbvmpo1 
|- ( x e. A , y e. B |-> C ) = ( z e. A , y e. B |-> E )

Proof

Step Hyp Ref Expression
1 cbvmpo1.1 
 |-  F/_ x B
2 cbvmpo1.2 
 |-  F/_ z B
3 cbvmpo1.3 
 |-  F/_ z C
4 cbvmpo1.4 
 |-  F/_ x E
5 cbvmpo1.5 
 |-  ( x = z -> C = E )
6 nfv 
 |-  F/ z x e. A
7 2 nfcri 
 |-  F/ z y e. B
8 6 7 nfan 
 |-  F/ z ( x e. A /\ y e. B )
9 3 nfeq2 
 |-  F/ z u = C
10 8 9 nfan 
 |-  F/ z ( ( x e. A /\ y e. B ) /\ u = C )
11 nfv 
 |-  F/ x z e. A
12 1 nfcri 
 |-  F/ x y e. B
13 11 12 nfan 
 |-  F/ x ( z e. A /\ y e. B )
14 4 nfeq2 
 |-  F/ x u = E
15 13 14 nfan 
 |-  F/ x ( ( z e. A /\ y e. B ) /\ u = E )
16 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
17 16 anbi1d 
 |-  ( x = z -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ y e. B ) ) )
18 5 eqeq2d 
 |-  ( x = z -> ( u = C <-> u = E ) )
19 17 18 anbi12d 
 |-  ( x = z -> ( ( ( x e. A /\ y e. B ) /\ u = C ) <-> ( ( z e. A /\ y e. B ) /\ u = E ) ) )
20 10 15 19 cbvoprab1 
 |-  { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) } = { <. <. z , y >. , u >. | ( ( z e. A /\ y e. B ) /\ u = E ) }
21 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , u >. | ( ( x e. A /\ y e. B ) /\ u = C ) }
22 df-mpo 
 |-  ( z e. A , y e. B |-> E ) = { <. <. z , y >. , u >. | ( ( z e. A /\ y e. B ) /\ u = E ) }
23 20 21 22 3eqtr4i 
 |-  ( x e. A , y e. B |-> C ) = ( z e. A , y e. B |-> E )