Metamath Proof Explorer


Theorem sbali

Description: Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

Ref Expression
Hypothesis sbali.1
|- A e. _V
Assertion sbali
|- ( [. A / x ]. A. x ph <-> A. x ph )

Proof

Step Hyp Ref Expression
1 sbali.1
 |-  A e. _V
2 nfa1
 |-  F/ x A. x ph
3 1 2 sbcgfi
 |-  ( [. A / x ]. A. x ph <-> A. x ph )