Metamath Proof Explorer

Theorem cbvmpox

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpo allows B to be a function of x . (Contributed by NM, 29-Dec-2014)

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

Proof

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