Step |
Hyp |
Ref |
Expression |
1 |
|
vtocl2gaf.a |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
vtocl2gaf.b |
⊢ Ⅎ 𝑦 𝐴 |
3 |
|
vtocl2gaf.c |
⊢ Ⅎ 𝑦 𝐵 |
4 |
|
vtocl2gaf.1 |
⊢ Ⅎ 𝑥 𝜓 |
5 |
|
vtocl2gaf.2 |
⊢ Ⅎ 𝑦 𝜒 |
6 |
|
vtocl2gaf.3 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
7 |
|
vtocl2gaf.4 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
8 |
|
vtocl2gaf.5 |
⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 ) |
9 |
2
|
nfel1 |
⊢ Ⅎ 𝑦 𝐴 ∈ 𝐶 |
10 |
9 5
|
nfim |
⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝐶 → 𝜒 ) |
11 |
7
|
imbi2d |
⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 → 𝜓 ) ↔ ( 𝐴 ∈ 𝐶 → 𝜒 ) ) ) |
12 |
|
nfv |
⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷 |
13 |
12 4
|
nfim |
⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐷 → 𝜓 ) |
14 |
6
|
imbi2d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ∈ 𝐷 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐷 → 𝜓 ) ) ) |
15 |
8
|
ex |
⊢ ( 𝑥 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜑 ) ) |
16 |
1 13 14 15
|
vtoclgaf |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜓 ) ) |
17 |
16
|
com12 |
⊢ ( 𝑦 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜓 ) ) |
18 |
3 10 11 17
|
vtoclgaf |
⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜒 ) ) |
19 |
18
|
impcom |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) |