Metamath Proof Explorer


Theorem r2alf

Description: Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016) Use r2allem . (Revised by Wolf Lammen, 9-Jan-2020)

Ref Expression
Hypothesis r2alf.1 _yA
Assertion r2alf xAyBφxyxAyBφ

Proof

Step Hyp Ref Expression
1 r2alf.1 _yA
2 1 nfcri yxA
3 2 19.21 yxAyBφxAyyBφ
4 3 r2allem xAyBφxyxAyBφ