Metamath Proof Explorer


Theorem nfbii

Description: Equality theorem for the nonfreeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)

Ref Expression
Hypothesis nfbii.1 φ ψ
Assertion nfbii x φ x ψ

Proof

Step Hyp Ref Expression
1 nfbii.1 φ ψ
2 nfbiit x φ ψ x φ x ψ
3 2 1 mpg x φ x ψ