Description: Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbviuneq12dv.xel | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 ) | |
cbviuneq12dv.yel | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 ) | ||
cbviuneq12dv.xsub | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 ) | ||
cbviuneq12dv.ysub | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 ) | ||
cbviuneq12dv.eq1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 ) | ||
cbviuneq12dv.eq2 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 ) | ||
Assertion | cbviuneq12dv | ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbviuneq12dv.xel | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐴 ) | |
2 | cbviuneq12dv.yel | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 ) | |
3 | cbviuneq12dv.xsub | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐹 ) | |
4 | cbviuneq12dv.ysub | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 ) | |
5 | cbviuneq12dv.eq1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐺 ) | |
6 | cbviuneq12dv.eq2 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐷 = 𝐹 ) | |
7 | nfv | ⊢ Ⅎ 𝑥 𝜑 | |
8 | nfv | ⊢ Ⅎ 𝑦 𝜑 | |
9 | nfcv | ⊢ Ⅎ 𝑥 𝑋 | |
10 | nfcv | ⊢ Ⅎ 𝑦 𝑌 | |
11 | nfcv | ⊢ Ⅎ 𝑥 𝐴 | |
12 | nfcv | ⊢ Ⅎ 𝑦 𝐴 | |
13 | nfcv | ⊢ Ⅎ 𝑦 𝐵 | |
14 | nfcv | ⊢ Ⅎ 𝑥 𝐶 | |
15 | nfcv | ⊢ Ⅎ 𝑦 𝐶 | |
16 | nfcv | ⊢ Ⅎ 𝑥 𝐷 | |
17 | nfcv | ⊢ Ⅎ 𝑥 𝐹 | |
18 | nfcv | ⊢ Ⅎ 𝑦 𝐺 | |
19 | 7 8 9 10 11 12 13 14 15 16 17 18 1 2 3 4 5 6 | cbviuneq12df | ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐶 𝐷 ) |