Metamath Proof Explorer

Theorem rexrsb

Description: An equivalent expression for restricted existence, analogous to exsb . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion rexrsb ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 rexsb ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
2 alral ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) )
3 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) )
4 19.27v ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ 𝑦 ∈ 𝐴 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ 𝑦 ∈ 𝐴 ) )
5 pm2.04 ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
6 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
7 6 biimprd ⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) )
8 7 imim1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) )
9 8 a2i ⊢ ( ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) )
10 pm2.04 ⊢ ( ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) )
11 5 9 10 3syl ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) )
12 11 imp ⊢ ( ( ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
13 12 alimi ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
14 4 13 sylbir ⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
15 14 ex ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝑦 → 𝜑 ) ) → ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
16 3 15 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
17 16 com12 ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
18 2 17 impbid2 ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) ) )
19 18 rexbiia ⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) )
20 1 19 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝜑 ) )