This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfiotadw

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 GG, 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 ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 𝜓 ) )