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 ⊢ Ⅎ _ y A
cbvmpo2.2 ⊢ Ⅎ _ w A
cbvmpo2.3 ⊢ Ⅎ _ w C
cbvmpo2.4 ⊢ Ⅎ _ y E
cbvmpo2.5 ⊢ y = w → C = E
Assertion cbvmpo2 ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , w ∈ B ⟼ E

Proof

Step Hyp Ref Expression
1 cbvmpo2.1 ⊢ Ⅎ _ y A
2 cbvmpo2.2 ⊢ Ⅎ _ w A
3 cbvmpo2.3 ⊢ Ⅎ _ w C
4 cbvmpo2.4 ⊢ Ⅎ _ y E
5 cbvmpo2.5 ⊢ y = w → C = E
6 2 nfcri ⊢ Ⅎ w x ∈ A
7 nfcv ⊢ Ⅎ _ w B
8 7 nfcri ⊢ Ⅎ w y ∈ B
9 6 8 nfan ⊢ Ⅎ w x ∈ A ∧ y ∈ B
10 3 nfeq2 ⊢ Ⅎ w u = C
11 9 10 nfan ⊢ Ⅎ w x ∈ A ∧ y ∈ B ∧ u = C
12 1 nfcri ⊢ Ⅎ y x ∈ A
13 nfv ⊢ Ⅎ y w ∈ B
14 12 13 nfan ⊢ Ⅎ y x ∈ A ∧ w ∈ B
15 4 nfeq2 ⊢ Ⅎ y u = E
16 14 15 nfan ⊢ Ⅎ y x ∈ A ∧ w ∈ B ∧ u = E
17 eleq1w ⊢ y = w → y ∈ B ↔ w ∈ B
18 17 anbi2d ⊢ y = w → x ∈ A ∧ y ∈ B ↔ x ∈ A ∧ w ∈ B
19 5 eqeq2d ⊢ y = w → u = C ↔ u = E
20 18 19 anbi12d ⊢ y = w → x ∈ A ∧ y ∈ B ∧ u = C ↔ x ∈ A ∧ w ∈ B ∧ u = E
21 11 16 20 cbvoprab2 ⊢ x y u | x ∈ A ∧ y ∈ B ∧ u = C = x w u | x ∈ A ∧ w ∈ B ∧ u = E
22 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y u | x ∈ A ∧ y ∈ B ∧ u = C
23 df-mpo ⊢ x ∈ A , w ∈ B ⟼ E = x w u | x ∈ A ∧ w ∈ B ∧ u = E
24 21 22 23 3eqtr4i ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , w ∈ B ⟼ E