Metamath Proof Explorer


Theorem snssgOLD

Description: Obsolete version of snssgOLD as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion snssgOLD ( 𝐴𝑉 → ( 𝐴𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 velsn ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
2 1 imbi1i ( ( 𝑥 ∈ { 𝐴 } → 𝑥𝐵 ) ↔ ( 𝑥 = 𝐴𝑥𝐵 ) )
3 2 albii ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) )
4 3 a1i ( 𝐴𝑉 → ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) ) )
5 dfss2 ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥𝐵 ) )
6 5 a1i ( 𝐴𝑉 → ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥𝐵 ) ) )
7 clel2g ( 𝐴𝑉 → ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝑥𝐵 ) ) )
8 4 6 7 3bitr4rd ( 𝐴𝑉 → ( 𝐴𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )