Metamath Proof Explorer


Theorem nfaba1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See nfaba1g for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024) Avoid ax-6 , ax-7 , ax-12 . (Revised by SN, 14-May-2025)

Ref Expression
Assertion nfaba1 𝑥 { 𝑦 ∣ ∀ 𝑥 𝜑 }

Proof

Step Hyp Ref Expression
1 df-clab ( 𝑧 ∈ { 𝑦 ∣ ∀ 𝑥 𝜑 } ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 )
2 sbal ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
3 nfa1 𝑥𝑥 [ 𝑧 / 𝑦 ] 𝜑
4 2 3 nfxfr 𝑥 [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑
5 1 4 nfxfr 𝑥 𝑧 ∈ { 𝑦 ∣ ∀ 𝑥 𝜑 }
6 5 nfci 𝑥 { 𝑦 ∣ ∀ 𝑥 𝜑 }