Description: Implicit substitution of a class for a setvar variable. Version of vtocl3gf with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by Gino Giotto, 3-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vtocl3g.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| vtocl3g.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | ||
| vtocl3g.3 | ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) ) | ||
| vtocl3g.4 | ⊢ 𝜑 | ||
| Assertion | vtocl3g | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝜃 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtocl3g.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | vtocl3g.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | |
| 3 | vtocl3g.3 | ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) ) | |
| 4 | vtocl3g.4 | ⊢ 𝜑 | |
| 5 | elex | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) | |
| 6 | 2 | imbi2d | ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ V → 𝜓 ) ↔ ( 𝐴 ∈ V → 𝜒 ) ) ) |
| 7 | 3 | imbi2d | ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 ∈ V → 𝜒 ) ↔ ( 𝐴 ∈ V → 𝜃 ) ) ) |
| 8 | 1 4 | vtoclg | ⊢ ( 𝐴 ∈ V → 𝜓 ) |
| 9 | 6 7 8 | vtocl2g | ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ V → 𝜃 ) ) |
| 10 | 5 9 | mpan9 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ) → 𝜃 ) |
| 11 | 10 | 3impb | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝜃 ) |