Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
nfraldw
Metamath Proof Explorer
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 Gino Giotto , 24-Sep-2024)
Ref
Expression
Hypotheses
nfraldw.1
|- F/ y ph
nfraldw.2
|- ( ph -> F/_ x A )
nfraldw.3
|- ( ph -> F/ x ps )
Assertion
nfraldw
|- ( ph -> F/ x A. y e. A ps )
Proof
Step
Hyp
Ref
Expression
1
nfraldw.1
|- F/ y ph
2
nfraldw.2
|- ( ph -> F/_ x A )
3
nfraldw.3
|- ( ph -> F/ x ps )
4
df-ral
|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
5
2
nfcrd
|- ( ph -> F/ x y e. A )
6
5 3
nfimd
|- ( ph -> F/ x ( y e. A -> ps ) )
7
1 6
nfald
|- ( ph -> F/ x A. y ( y e. A -> ps ) )
8
4 7
nfxfrd
|- ( ph -> F/ x A. y e. A ps )