Metamath Proof Explorer


Theorem bj-cbveximi

Description: An equality-free general instance of one half of a precise form of bj-cbvex . (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbvalimi.maj ( 𝜒 → ( 𝜑𝜓 ) )
bj-cbveximi.denote 𝑥𝑦 𝜒
Assertion bj-cbveximi ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 bj-cbvalimi.maj ( 𝜒 → ( 𝜑𝜓 ) )
2 bj-cbveximi.denote 𝑥𝑦 𝜒
3 1 gen2 𝑥𝑦 ( 𝜒 → ( 𝜑𝜓 ) )
4 bj-cbvexim ( ∀ 𝑥𝑦 𝜒 → ( ∀ 𝑥𝑦 ( 𝜒 → ( 𝜑𝜓 ) ) → ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 ) ) )
5 2 3 4 mp2 ( ∃ 𝑥 𝜑 → ∃ 𝑦 𝜓 )