Description: A lemma for alpha-renaming of variables bound by a universal quantifier. Hypothesis bj-cbvalimdlem.nfch can be proved either from DV conditions as in bj-cbvalimdv or from a nonfreeness condition and alcom as in bj-cbvalimd . Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 , and this proof is therefore a bit longer, not using bj-spim but bj-eximcom . (Contributed by BJ, 12-Mar-2023) Proof should not use 19.35 . (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-cbvalimdlem.nf0 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| bj-cbvalimdlem.nf1 | ⊢ ( 𝜑 → ∀ 𝑦 𝜑 ) | ||
| bj-cbvalimdlem.nfch | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 ∀ 𝑥 𝜒 ) ) | ||
| bj-cbvalimdlem.nfth | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) ) | ||
| bj-cbvalimdlem.denote | ⊢ ( 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) | ||
| bj-cbvalimdlem.maj | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) ) | ||
| Assertion | bj-cbvalimdlem | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 𝜃 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-cbvalimdlem.nf0 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| 2 | bj-cbvalimdlem.nf1 | ⊢ ( 𝜑 → ∀ 𝑦 𝜑 ) | |
| 3 | bj-cbvalimdlem.nfch | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 ∀ 𝑥 𝜒 ) ) | |
| 4 | bj-cbvalimdlem.nfth | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) ) | |
| 5 | bj-cbvalimdlem.denote | ⊢ ( 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) | |
| 6 | bj-cbvalimdlem.maj | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) ) | |
| 7 | 6 | ex | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) |
| 8 | 1 7 | eximdh | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑥 ( 𝜒 → 𝜃 ) ) ) |
| 9 | 2 8 | alimdh | ⊢ ( 𝜑 → ( ∀ 𝑦 ∃ 𝑥 𝜓 → ∀ 𝑦 ∃ 𝑥 ( 𝜒 → 𝜃 ) ) ) |
| 10 | 5 9 | mpd | ⊢ ( 𝜑 → ∀ 𝑦 ∃ 𝑥 ( 𝜒 → 𝜃 ) ) |
| 11 | bj-eximcom | ⊢ ( ∃ 𝑥 ( 𝜒 → 𝜃 ) → ( ∀ 𝑥 𝜒 → ∃ 𝑥 𝜃 ) ) | |
| 12 | 10 3 11 | bj-alrimd | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 ∃ 𝑥 𝜃 ) ) |
| 13 | 2 12 4 | bj-alrimd | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 𝜃 ) ) |