Description: Version of cbv1h with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbv1hv.1 | ⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑦 𝜓 ) ) | |
bj-cbv1hv.2 | ⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) ) | ||
bj-cbv1hv.3 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) | ||
Assertion | bj-cbv1hv | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbv1hv.1 | ⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑦 𝜓 ) ) | |
2 | bj-cbv1hv.2 | ⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) ) | |
3 | bj-cbv1hv.3 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) | |
4 | nfa1 | ⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 𝜑 | |
5 | nfa2 | ⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 𝜑 | |
6 | 2sp | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → 𝜑 ) | |
7 | 6 1 | syl | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( 𝜓 → ∀ 𝑦 𝜓 ) ) |
8 | 5 7 | nf5d | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → Ⅎ 𝑦 𝜓 ) |
9 | 6 2 | syl | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( 𝜒 → ∀ 𝑥 𝜒 ) ) |
10 | 4 9 | nf5d | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → Ⅎ 𝑥 𝜒 ) |
11 | 6 3 | syl | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) |
12 | 4 5 8 10 11 | cbv1v | ⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) ) |