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 nfraldw
Description: Deduction version of nfralw . Version of nfrald with a disjoint
variable condition, which does not require ax-13 . (Contributed by NM , 15-Feb-2013) Avoid ax-9 , ax-ext . (Revised by GG , 24-Sep-2024)
Ref
Expression
Hypotheses
nfraldw.1 ⊢ Ⅎ 𝑦 𝜑
nfraldw.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
nfraldw.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion
nfraldw ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜓 )
Proof
Step
Hyp
Ref
Expression
1
nfraldw.1 ⊢ Ⅎ 𝑦 𝜑
2
nfraldw.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3
nfraldw.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
4
df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
5
2
nfcrd ⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
6
5 3
nfimd ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
7
1 6
nfald ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
8
4 7
nfxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 𝜓 )