Metamath Proof Explorer

Theorem bj-cbveximdlem

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 ⊢ φ → ∀ x φ
bj-cbveximdlem.nf1 ⊢ φ → ∀ y φ
bj-cbveximdlem.nfch ⊢ φ → χ → ∀ y χ
bj-cbveximdlem.nfth ⊢ φ → ∃ x ∃ y θ → ∃ y θ
bj-cbveximdlem.denote ⊢ φ → ∀ x ∃ y ψ
bj-cbveximdlem.maj ⊢ φ ∧ ψ → χ → θ
Assertion bj-cbveximdlem ⊢ φ → ∃ x χ → ∃ y θ

Proof

Step Hyp Ref Expression
1 bj-cbveximdlem.nf0 ⊢ φ → ∀ x φ
2 bj-cbveximdlem.nf1 ⊢ φ → ∀ y φ
3 bj-cbveximdlem.nfch ⊢ φ → χ → ∀ y χ
4 bj-cbveximdlem.nfth ⊢ φ → ∃ x ∃ y θ → ∃ y θ
5 bj-cbveximdlem.denote ⊢ φ → ∀ x ∃ y ψ
6 bj-cbveximdlem.maj ⊢ φ ∧ ψ → χ → θ
7 6 ex ⊢ φ → ψ → χ → θ
8 2 7 eximdh ⊢ φ → ∃ y ψ → ∃ y χ → θ
9 1 8 alimdh ⊢ φ → ∀ x ∃ y ψ → ∀ x ∃ y χ → θ
10 5 9 mpd ⊢ φ → ∀ x ∃ y χ → θ
11 bj-eximcom ⊢ ∃ y χ → θ → ∀ y χ → ∃ y θ
12 10 4 11 bj-exlimd ⊢ φ → ∃ x ∀ y χ → ∃ y θ
13 1 12 3 bj-exlimd ⊢ φ → ∃ x χ → ∃ y θ