Metamath Proof Explorer


Theorem rgen2w

Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by NM, 18-Jun-2014)

Ref Expression
Hypothesis rgenw.1 φ
Assertion rgen2w x A y B φ

Proof

Step Hyp Ref Expression
1 rgenw.1 φ
2 1 rgenw y B φ
3 2 rgenw x A y B φ