This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification r2alf
Description: Double restricted universal quantification. For a version based on
fewer axioms see r2al . (Contributed by Mario Carneiro , 14-Oct-2016)
Use r2allem . (Revised by Wolf Lammen , 9-Jan-2020)
Ref
Expression
Hypothesis
r2alf.1 ⊢ Ⅎ _ y A
Assertion
r2alf ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ
Proof
Step
Hyp
Ref
Expression
1
r2alf.1 ⊢ Ⅎ _ y A
2
1
nfcri ⊢ Ⅎ y x ∈ A
3
2
19.21 ⊢ ∀ y x ∈ A → y ∈ B → φ ↔ x ∈ A → ∀ y y ∈ B → φ
4
3
r2allem ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ