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 V
Assertion sbali [˙A / x]˙ x φ x φ

Proof

Step Hyp Ref Expression
1 sbali.1 A V
2 nfa1 x x φ
3 1 2 sbcgfi [˙A / x]˙ x φ x φ