Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vtocl2ga.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| vtocl2ga.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | ||
| vtocl2ga.3 | ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 ) | ||
| Assertion | vtocl2ga | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtocl2ga.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | vtocl2ga.2 | ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) | |
| 3 | vtocl2ga.3 | ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 ) | |
| 4 | 2 | imbi2d | ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 → 𝜓 ) ↔ ( 𝐴 ∈ 𝐶 → 𝜒 ) ) ) |
| 5 | 1 | imbi2d | ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ∈ 𝐷 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐷 → 𝜓 ) ) ) |
| 6 | 3 | ex | ⊢ ( 𝑥 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜑 ) ) |
| 7 | 5 6 | vtoclga | ⊢ ( 𝐴 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜓 ) ) |
| 8 | 7 | com12 | ⊢ ( 𝑦 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜓 ) ) |
| 9 | 4 8 | vtoclga | ⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜒 ) ) |
| 10 | 9 | impcom | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) |