Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Definite description binder (inverted iota)
nfiotadw
Metamath Proof Explorer
Description: Deduction version of nfiotaw . Version of nfiotad with a disjoint
variable condition, which does not require ax-13 . (Contributed by NM , 18-Feb-2013) Avoid ax-13 . (Revised by Gino Giotto , 26-Jan-2024)
Ref
Expression
Hypotheses
nfiotadw.1
⊢ Ⅎ 𝑦 𝜑
nfiotadw.2
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion
nfiotadw
⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
nfiotadw.1
⊢ Ⅎ 𝑦 𝜑
2
nfiotadw.2
⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3
dfiota2
⊢ ( ℩ 𝑦 𝜓 ) = ∪ { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) }
4
nfv
⊢ Ⅎ 𝑧 𝜑
5
nfvd
⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = 𝑧 )
6
2 5
nfbid
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜓 ↔ 𝑦 = 𝑧 ) )
7
1 6
nfald
⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) )
8
4 7
nfabdw
⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) } )
9
8
nfunid
⊢ ( 𝜑 → Ⅎ 𝑥 ∪ { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) } )
10
3 9
nfcxfrd
⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 𝜓 ) )