Metamath Proof Explorer


Theorem rexcom4f

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

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

Proof

Step Hyp Ref Expression
1 ralcom4f.1 _ y A
2 nfcv _ x V
3 1 2 rexcomf x A y V φ y V x A φ
4 rexv y V φ y φ
5 4 rexbii x A y V φ x A y φ
6 rexv y V x A φ y x A φ
7 3 5 6 3bitr3i x A y φ y x A φ