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

Proof

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