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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr | ||
2 | df-rex | ||
3 | 2 | exbii | |
4 | excom | ||
5 | 3 4 | bitri | |
6 | df-rex | ||
7 | 1 5 6 | 3bitr4ri |