Metamath Proof Explorer

Theorem cbvmpox2

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows A to be a function of y , analogous to cbvmpox . (Contributed by AV, 30-Mar-2019)

Ref Expression
Hypotheses cbvmpox2.1 ⊢ Ⅎ _ z A
cbvmpox2.2 ⊢ Ⅎ _ y D
cbvmpox2.3 ⊢ Ⅎ _ z C
cbvmpox2.4 ⊢ Ⅎ _ w C
cbvmpox2.5 ⊢ Ⅎ _ x E
cbvmpox2.6 ⊢ Ⅎ _ y E
cbvmpox2.7 ⊢ y = z → A = D
cbvmpox2.8 ⊢ y = z ∧ x = w → C = E
Assertion cbvmpox2 ⊢ x ∈ A , y ∈ B ⟼ C = w ∈ D , z ∈ B ⟼ E

Proof

Step Hyp Ref Expression
1 cbvmpox2.1 ⊢ Ⅎ _ z A
2 cbvmpox2.2 ⊢ Ⅎ _ y D
3 cbvmpox2.3 ⊢ Ⅎ _ z C
4 cbvmpox2.4 ⊢ Ⅎ _ w C
5 cbvmpox2.5 ⊢ Ⅎ _ x E
6 cbvmpox2.6 ⊢ Ⅎ _ y E
7 cbvmpox2.7 ⊢ y = z → A = D
8 cbvmpox2.8 ⊢ y = z ∧ x = w → C = E
9 nfv ⊢ Ⅎ w x ∈ A
10 nfv ⊢ Ⅎ w y ∈ B
11 9 10 nfan ⊢ Ⅎ w x ∈ A ∧ y ∈ B
12 4 nfeq2 ⊢ Ⅎ w u = C
13 11 12 nfan ⊢ Ⅎ w x ∈ A ∧ y ∈ B ∧ u = C
14 1 nfcri ⊢ Ⅎ z x ∈ A
15 nfv ⊢ Ⅎ z y ∈ B
16 14 15 nfan ⊢ Ⅎ z x ∈ A ∧ y ∈ B
17 3 nfeq2 ⊢ Ⅎ z u = C
18 16 17 nfan ⊢ Ⅎ z x ∈ A ∧ y ∈ B ∧ u = C
19 nfv ⊢ Ⅎ x w ∈ D
20 nfv ⊢ Ⅎ x z ∈ B
21 19 20 nfan ⊢ Ⅎ x w ∈ D ∧ z ∈ B
22 5 nfeq2 ⊢ Ⅎ x u = E
23 21 22 nfan ⊢ Ⅎ x w ∈ D ∧ z ∈ B ∧ u = E
24 2 nfcri ⊢ Ⅎ y w ∈ D
25 nfv ⊢ Ⅎ y z ∈ B
26 24 25 nfan ⊢ Ⅎ y w ∈ D ∧ z ∈ B
27 6 nfeq2 ⊢ Ⅎ y u = E
28 26 27 nfan ⊢ Ⅎ y w ∈ D ∧ z ∈ B ∧ u = E
29 eleq1w ⊢ x = w → x ∈ A ↔ w ∈ A
30 7 eleq2d ⊢ y = z → w ∈ A ↔ w ∈ D
31 29 30 sylan9bb ⊢ x = w ∧ y = z → x ∈ A ↔ w ∈ D
32 simpr ⊢ x = w ∧ y = z → y = z
33 32 eleq1d ⊢ x = w ∧ y = z → y ∈ B ↔ z ∈ B
34 31 33 anbi12d ⊢ x = w ∧ y = z → x ∈ A ∧ y ∈ B ↔ w ∈ D ∧ z ∈ B
35 8 ancoms ⊢ x = w ∧ y = z → C = E
36 35 eqeq2d ⊢ x = w ∧ y = z → u = C ↔ u = E
37 34 36 anbi12d ⊢ x = w ∧ y = z → x ∈ A ∧ y ∈ B ∧ u = C ↔ w ∈ D ∧ z ∈ B ∧ u = E
38 13 18 23 28 37 cbvoprab12 ⊢ x y u | x ∈ A ∧ y ∈ B ∧ u = C = w z u | w ∈ D ∧ z ∈ B ∧ u = E
39 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y u | x ∈ A ∧ y ∈ B ∧ u = C
40 df-mpo ⊢ w ∈ D , z ∈ B ⟼ E = w z u | w ∈ D ∧ z ∈ B ∧ u = E
41 38 39 40 3eqtr4i ⊢ x ∈ A , y ∈ B ⟼ C = w ∈ D , z ∈ B ⟼ E