Metamath Proof Explorer

Theorem bj-cbvalimdlem

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

Proof

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