Metamath Proof Explorer


Theorem bj-cbvexim

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

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

Proof

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