Metamath Proof Explorer


Theorem rexcom4

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019)

Ref Expression
Assertion rexcom4 x A y φ y x A φ

Proof

Step Hyp Ref Expression
1 exdistr x y x A φ x x A y φ
2 df-rex x A φ x x A φ
3 2 exbii y x A φ y x x A φ
4 excom y x x A φ x y x A φ
5 3 4 bitri y x A φ x y x A φ
6 df-rex x A y φ x x A y φ
7 1 5 6 3bitr4ri x A y φ y x A φ