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 ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∃ 𝑦𝐵𝑥𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑦𝐵 𝜑 ↔ ∃ 𝑦 ( 𝑦𝐵𝜑 ) )
2 1 rexbii ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∃ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) )
3 rexcom4 ( ∃ 𝑥𝐴𝑦 ( 𝑦𝐵𝜑 ) ↔ ∃ 𝑦𝑥𝐴 ( 𝑦𝐵𝜑 ) )
4 r19.42v ( ∃ 𝑥𝐴 ( 𝑦𝐵𝜑 ) ↔ ( 𝑦𝐵 ∧ ∃ 𝑥𝐴 𝜑 ) )
5 4 exbii ( ∃ 𝑦𝑥𝐴 ( 𝑦𝐵𝜑 ) ↔ ∃ 𝑦 ( 𝑦𝐵 ∧ ∃ 𝑥𝐴 𝜑 ) )
6 df-rex ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ↔ ∃ 𝑦 ( 𝑦𝐵 ∧ ∃ 𝑥𝐴 𝜑 ) )
7 5 6 bitr4i ( ∃ 𝑦𝑥𝐴 ( 𝑦𝐵𝜑 ) ↔ ∃ 𝑦𝐵𝑥𝐴 𝜑 )
8 2 3 7 3bitri ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∃ 𝑦𝐵𝑥𝐴 𝜑 )