This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabeqsnd

Description: Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021)

Ref Expression
Hypotheses rabeqsnd.0 ⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
rabeqsnd.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
rabeqsnd.2 ⊢ ( 𝜑 → 𝜒 )
rabeqsnd.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 = 𝐵 )
Assertion rabeqsnd ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } )

Proof

Step Hyp Ref Expression
1 rabeqsnd.0 ⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2 rabeqsnd.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3 rabeqsnd.2 ⊢ ( 𝜑 → 𝜒 )
4 rabeqsnd.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝑥 = 𝐵 )
5 4 expl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) )
6 5 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) )
7 2 3 jca ⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) )
8 7 a1d ⊢ ( 𝜑 → ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
9 8 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
10 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
11 10 1 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
12 11 pm5.74i ⊢ ( ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
13 12 albii ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝐵 ∈ 𝐴 ∧ 𝜒 ) ) )
14 9 13 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
15 6 14 jca ⊢ ( 𝜑 → ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) )
16 albiim ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) ↔ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝑥 = 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) )
17 15 16 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) )
18 rabeqsn ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ 𝑥 = 𝐵 ) )
19 17 18 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝐵 } )