Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
reximiaOLD
Metamath Proof Explorer
Description: Obsolete version of reximia as of 31-Oct-2024. (Contributed by NM , 10-Feb-1997) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypothesis
reximiaOLD.1
⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
Assertion
reximiaOLD
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
reximiaOLD.1
⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) )
2
rexim
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
3
2 1
mprg
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )