Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
r19.29vva
Metamath Proof Explorer
Description: A commonly used pattern based on r19.29 , version with two restricted
quantifiers. (Contributed by Thierry Arnoux , 26-Nov-2017) (Proof
shortened by Wolf Lammen , 29-Jun-2023)
Ref
Expression
Hypotheses
r19.29vva.1
⊢ φ ∧ x ∈ A ∧ y ∈ B ∧ ψ → χ
r19.29vva.2
⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ
Assertion
r19.29vva
⊢ φ → χ
Proof
Step
Hyp
Ref
Expression
1
r19.29vva.1
⊢ φ ∧ x ∈ A ∧ y ∈ B ∧ ψ → χ
2
r19.29vva.2
⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ
3
1 2
reximddv2
⊢ φ → ∃ x ∈ A ∃ y ∈ B χ
4
id
⊢ χ → χ
5
4
rexlimivw
⊢ ∃ y ∈ B χ → χ
6
5
reximi
⊢ ∃ x ∈ A ∃ y ∈ B χ → ∃ x ∈ A χ
7
4
rexlimivw
⊢ ∃ x ∈ A χ → χ
8
3 6 7
3syl
⊢ φ → χ