Metamath Proof Explorer


Theorem bj-exlimmpi

Description: Lemma for bj-vtoclg1f1 (an instance of this lemma is a version of bj-vtoclg1f1 where x and y are identified). (Contributed by BJ, 30-Apr-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-exlimmpi.nf 𝑥 𝜓
bj-exlimmpi.maj ( 𝜒 → ( 𝜑𝜓 ) )
bj-exlimmpi.min 𝜑
Assertion bj-exlimmpi ( ∃ 𝑥 𝜒𝜓 )

Proof

Step Hyp Ref Expression
1 bj-exlimmpi.nf 𝑥 𝜓
2 bj-exlimmpi.maj ( 𝜒 → ( 𝜑𝜓 ) )
3 bj-exlimmpi.min 𝜑
4 3 2 mpi ( 𝜒𝜓 )
5 1 4 exlimi ( ∃ 𝑥 𝜒𝜓 )