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 ralbid
Description: Formula-building rule for restricted universal quantifier (deduction
form). For a version based on fewer axioms see ralbidv .
(Contributed by NM , 27-Jun-1998)
Ref
Expression
Hypotheses
ralbid.1 ⊢ Ⅎ x φ
ralbid.2 ⊢ φ → ψ ↔ χ
Assertion
ralbid ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A χ
Proof
Step
Hyp
Ref
Expression
1
ralbid.1 ⊢ Ⅎ x φ
2
ralbid.2 ⊢ φ → ψ ↔ χ
3
2
adantr ⊢ φ ∧ x ∈ A → ψ ↔ χ
4
1 3
ralbida ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A χ