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

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 GG, 20-Jan-2024) Avoid ax-12 . (Revised by SN, 14-May-2025)

Ref Expression
Assertion nfaba1 ⊢ Ⅎ _ x y | ∀ x φ

Proof

Step Hyp Ref Expression
1 df-clab ⊢ z ∈ y | ∀ x φ ↔ z y ∀ x φ
2 sbal ⊢ z y ∀ x φ ↔ ∀ x z y φ
3 nfa1 ⊢ Ⅎ x ∀ x z y φ
4 2 3 nfxfr ⊢ Ⅎ x z y ∀ x φ
5 1 4 nfxfr ⊢ Ⅎ x z ∈ y | ∀ x φ
6 5 nfci ⊢ Ⅎ _ x y | ∀ x φ