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