Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
reximia
Next ⟩
reximi
Metamath Proof Explorer
Ascii
Unicode
Theorem
reximia
Description:
Inference quantifying both antecedent and consequent.
(Contributed by
NM
, 10-Feb-1997)
Ref
Expression
Hypothesis
reximia.1
⊢
x
∈
A
→
φ
→
ψ
Assertion
reximia
⊢
∃
x
∈
A
φ
→
∃
x
∈
A
ψ
Proof
Step
Hyp
Ref
Expression
1
reximia.1
⊢
x
∈
A
→
φ
→
ψ
2
rexim
⊢
∀
x
∈
A
φ
→
ψ
→
∃
x
∈
A
φ
→
∃
x
∈
A
ψ
3
2
1
mprg
⊢
∃
x
∈
A
φ
→
∃
x
∈
A
ψ