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

Proof

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