Metamath Proof Explorer

Theorem rexcomf

Description: Commutation of restricted existential quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses ralcomf.1 
|- F/_ y A
ralcomf.2 
|- F/_ x B
Assertion rexcomf 
|- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )

Proof

Step Hyp Ref Expression
1 ralcomf.1 
 |-  F/_ y A
2 ralcomf.2 
 |-  F/_ x B
3 ancom 
 |-  ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) )
4 3 anbi1i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ph ) <-> ( ( y e. B /\ x e. A ) /\ ph ) )
5 4 2exbii 
 |-  ( E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> E. x E. y ( ( y e. B /\ x e. A ) /\ ph ) )
6 excom 
 |-  ( E. x E. y ( ( y e. B /\ x e. A ) /\ ph ) <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
7 5 6 bitri 
 |-  ( E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
8 1 r2exf 
 |-  ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
9 2 r2exf 
 |-  ( E. y e. B E. x e. A ph <-> E. y E. x ( ( y e. B /\ x e. A ) /\ ph ) )
10 7 8 9 3bitr4i 
 |-  ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )