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

Metamath Proof Explorer

Theorem cbvmpo2

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

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

Proof

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