Metamath Proof Explorer


Theorem rabexgf

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

Ref Expression
Hypothesis rabexgf.1 _ x A
Assertion rabexgf A V x A | φ V

Proof

Step Hyp Ref Expression
1 rabexgf.1 _ x A
2 df-rab x A | φ = x | x A φ
3 simpl x A φ x A
4 3 ss2abi x | x A φ x | x A
5 1 abid2f x | x A = A
6 4 5 sseqtri x | x A φ A
7 2 6 eqsstri x A | φ A
8 ssexg x A | φ A A V x A | φ V
9 7 8 mpan A V x A | φ V