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

Metamath Proof Explorer

Theorem snssb

Description: Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025)

Ref Expression
Assertion snssb ( { 𝐴 } ⊆ 𝐵 ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-ss ⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
2 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3 2 imbi1i ⊢ ( ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
4 3 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
5 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
6 5 pm5.74i ⊢ ( ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
7 6 albii ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
8 19.23v ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
9 isset ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
10 9 bicomi ⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ V )
11 10 imbi1i ⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )
12 7 8 11 3bitri ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )
13 1 4 12 3bitri ⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )