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 ( 𝜑 → { 𝑥𝐴𝜓 } = { 𝐵 } )