Metamath Proof Explorer


Theorem bj-cbvalim

Description: A lemma used to prove bj-cbval in a weak axiomatization. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-cbvalim ( ∀ 𝑦𝑥 𝜒 → ( ∀ 𝑦𝑥 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 ax5e ( ∃ 𝑥 𝜓𝜓 )
2 1 ax-gen 𝑦 ( ∃ 𝑥 𝜓𝜓 )
3 ax-5 ( ∀ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 )
4 bj-cbvalimt ( ∀ 𝑦𝑥 𝜒 → ( ∀ 𝑦𝑥 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) )
5 4 com3l ( ∀ 𝑦𝑥 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) → ( ∀ 𝑦𝑥 𝜒 → ( ∀ 𝑦 ( ∃ 𝑥 𝜓𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) )
6 5 com14 ( ∀ 𝑦 ( ∃ 𝑥 𝜓𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦𝑥 𝜑 ) → ( ∀ 𝑦𝑥 𝜒 → ( ∀ 𝑦𝑥 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) )
7 2 3 6 mp2 ( ∀ 𝑦𝑥 𝜒 → ( ∀ 𝑦𝑥 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) )