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 
|- F/_ x { y | A. x ph }

Proof

Step Hyp Ref Expression
1 df-clab 
 |-  ( z e. { y | A. x ph } <-> [ z / y ] A. x ph )
2 sbal 
 |-  ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
3 nfa1 
 |-  F/ x A. x [ z / y ] ph
4 2 3 nfxfr 
 |-  F/ x [ z / y ] A. x ph
5 1 4 nfxfr 
 |-  F/ x z e. { y | A. x ph }
6 5 nfci 
 |-  F/_ x { y | A. x ph }