Metamath Proof Explorer


Theorem rexlimivOLD

Description: Obsolete version of rexlimiv as of 19-Dec-2024.) (Contributed by NM, 20-Nov-1994) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rexlimivOLD.1 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
Assertion rexlimivOLD ( ∃ 𝑥𝐴 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 rexlimivOLD.1 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
2 1 rgen 𝑥𝐴 ( 𝜑𝜓 )
3 r19.23v ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥𝐴 𝜑𝜓 ) )
4 2 3 mpbi ( ∃ 𝑥𝐴 𝜑𝜓 )