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 x A =
Assertion rzalf A = x A φ

Proof

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