Metamath Proof Explorer


Theorem rexcomOLD

Description: Obsolete version of rexcom as of 8-Dec-2024. (Contributed by NM, 19-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016) (Proof shortened by BJ, 26-Aug-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion rexcomOLD
|- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )

Proof

Step Hyp Ref Expression
1 df-rex
 |-  ( E. y e. B ph <-> E. y ( y e. B /\ ph ) )
2 1 rexbii
 |-  ( E. x e. A E. y e. B ph <-> E. x e. A E. y ( y e. B /\ ph ) )
3 rexcom4
 |-  ( E. x e. A E. y ( y e. B /\ ph ) <-> E. y E. x e. A ( y e. B /\ ph ) )
4 r19.42v
 |-  ( E. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ E. x e. A ph ) )
5 4 exbii
 |-  ( E. y E. x e. A ( y e. B /\ ph ) <-> E. y ( y e. B /\ E. x e. A ph ) )
6 df-rex
 |-  ( E. y e. B E. x e. A ph <-> E. y ( y e. B /\ E. x e. A ph ) )
7 5 6 bitr4i
 |-  ( E. y E. x e. A ( y e. B /\ ph ) <-> E. y e. B E. x e. A ph )
8 2 3 7 3bitri
 |-  ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )