Metamath Proof Explorer
Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995)
|
|
Ref |
Expression |
|
Hypotheses |
vtocl3ga.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
|
|
vtocl3ga.2 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
|
|
vtocl3ga.3 |
⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) ) |
|
|
vtocl3ga.4 |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆 ) → 𝜑 ) |
|
Assertion |
vtocl3ga |
⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆 ) → 𝜃 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
vtocl3ga.1 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
vtocl3ga.2 |
⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) |
3 |
|
vtocl3ga.3 |
⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) ) |
4 |
|
vtocl3ga.4 |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆 ) → 𝜑 ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
6 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐴 |
7 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐴 |
8 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐵 |
9 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐵 |
10 |
|
nfcv |
⊢ Ⅎ 𝑧 𝐶 |
11 |
|
nfv |
⊢ Ⅎ 𝑥 𝜓 |
12 |
|
nfv |
⊢ Ⅎ 𝑦 𝜒 |
13 |
|
nfv |
⊢ Ⅎ 𝑧 𝜃 |
14 |
5 6 7 8 9 10 11 12 13 1 2 3 4
|
vtocl3gaf |
⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆 ) → 𝜃 ) |