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

Metamath Proof Explorer

Theorem nfiotad

Description: Deduction version of nfiota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfiotadw when possible. (Contributed by NM, 18-Feb-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nfiotad.1 ⊢ Ⅎ 𝑦 𝜑
nfiotad.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
Assertion nfiotad ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 𝜓 ) )

Proof

Step Hyp Ref Expression
1 nfiotad.1 ⊢ Ⅎ 𝑦 𝜑
2 nfiotad.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 dfiota2 ⊢ ( ℩ 𝑦 𝜓 ) = ∪ { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) }
4 nfv ⊢ Ⅎ 𝑧 𝜑
5 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
6 nfeqf1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 = 𝑧 )
7 6 adantl ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 = 𝑧 )
8 5 7 nfbid ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝜓 ↔ 𝑦 = 𝑧 ) )
9 1 8 nfald2 ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) )
10 4 9 nfabd ⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) } )
11 10 nfunid ⊢ ( 𝜑 → Ⅎ 𝑥 ∪ { 𝑧 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑧 ) } )
12 3 11 nfcxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 𝜓 ) )