Metamath Proof Explorer


Theorem rzalf

Description: A version of rzal using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypothesis rzalf.1 xA=
Assertion rzalf A=xAφ

Proof

Step Hyp Ref Expression
1 rzalf.1 xA=
2 ne0i xAA
3 2 necon2bi A=¬xA
4 3 pm2.21d A=xAφ
5 1 4 ralrimi A=xAφ