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 ⊢ Ⅎ 𝑧 𝐵
cbvmpox.2 ⊢ Ⅎ 𝑥 𝐷
cbvmpox.3 ⊢ Ⅎ 𝑧 𝐶
cbvmpox.4 ⊢ Ⅎ 𝑤 𝐶
cbvmpox.5 ⊢ Ⅎ 𝑥 𝐸
cbvmpox.6 ⊢ Ⅎ 𝑦 𝐸
cbvmpox.7 ⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐷 )
cbvmpox.8 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐸 )
Assertion cbvmpox ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 )

Proof

Step Hyp Ref Expression
1 cbvmpox.1 ⊢ Ⅎ 𝑧 𝐵
2 cbvmpox.2 ⊢ Ⅎ 𝑥 𝐷
3 cbvmpox.3 ⊢ Ⅎ 𝑧 𝐶
4 cbvmpox.4 ⊢ Ⅎ 𝑤 𝐶
5 cbvmpox.5 ⊢ Ⅎ 𝑥 𝐸
6 cbvmpox.6 ⊢ Ⅎ 𝑦 𝐸
7 cbvmpox.7 ⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐷 )
8 cbvmpox.8 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝐶 = 𝐸 )
9 nfv ⊢ Ⅎ 𝑧 𝑥 ∈ 𝐴
10 1 nfcri ⊢ Ⅎ 𝑧 𝑦 ∈ 𝐵
11 9 10 nfan ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
12 3 nfeq2 ⊢ Ⅎ 𝑧 𝑢 = 𝐶
13 11 12 nfan ⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 )
14 nfv ⊢ Ⅎ 𝑤 𝑥 ∈ 𝐴
15 nfcv ⊢ Ⅎ 𝑤 𝐵
16 15 nfcri ⊢ Ⅎ 𝑤 𝑦 ∈ 𝐵
17 14 16 nfan ⊢ Ⅎ 𝑤 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
18 4 nfeq2 ⊢ Ⅎ 𝑤 𝑢 = 𝐶
19 17 18 nfan ⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 )
20 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
21 2 nfcri ⊢ Ⅎ 𝑥 𝑤 ∈ 𝐷
22 20 21 nfan ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 )
23 5 nfeq2 ⊢ Ⅎ 𝑥 𝑢 = 𝐸
24 22 23 nfan ⊢ Ⅎ 𝑥 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 )
25 nfv ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 )
26 6 nfeq2 ⊢ Ⅎ 𝑦 𝑢 = 𝐸
27 25 26 nfan ⊢ Ⅎ 𝑦 ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 )
28 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
29 28 adantr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
30 7 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐷 ) )
31 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝐷 ↔ 𝑤 ∈ 𝐷 ) )
32 30 31 sylan9bb ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐷 ) )
33 29 32 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ) )
34 8 eqeq2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑢 = 𝐶 ↔ 𝑢 = 𝐸 ) )
35 33 34 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) ) )
36 13 19 24 27 35 cbvoprab12 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) } = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) }
37 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = 𝐶 ) }
38 df-mpo ⊢ ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 ) = { ⟨ ⟨ 𝑧 , 𝑤 ⟩ , 𝑢 ⟩ ∣ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 = 𝐸 ) }
39 36 37 38 3eqtr4i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ 𝐴 , 𝑤 ∈ 𝐷 ↦ 𝐸 )