Theorem nfiota1

Description: Bound-variable hypothesis builder for the iota class. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Assertion	nfiota1	⊢ Ⅎ 𝑥 ( ℩ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
2		nfaba1	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
3	2	nfuni	⊢ Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) }
4	1 3	nfcxfr	⊢ Ⅎ 𝑥 ( ℩ 𝑥 𝜑 )