Metamath Proof Explorer

Theorem ralcom4f

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypothesis ralcom4f.1 _ y A
Assertion ralcom4f x A y φ y x A φ


Step Hyp Ref Expression
1 ralcom4f.1 _ y A
2 nfcv _ x V
3 1 2 ralcomf x A y V φ y V x A φ
4 ralv y V φ y φ
5 4 ralbii x A y V φ x A y φ
6 ralv y V x A φ y x A φ
7 3 5 6 3bitr3i x A y φ y x A φ