Metamath Proof Explorer

Theorem snssiALTVD

Description: Virtual deduction proof of snssiALT . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion snssiALTVD 
|- ( A e. B -> { A } C_ B )

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
2 idn1 
 |-  (. A e. B ->. A e. B ).
3 idn2 
 |-  (. A e. B ,. x e. { A } ->. x e. { A } ).
4 velsn 
 |-  ( x e. { A } <-> x = A )
5 3 4 e2bi 
 |-  (. A e. B ,. x e. { A } ->. x = A ).
6 eleq1a 
 |-  ( A e. B -> ( x = A -> x e. B ) )
7 2 5 6 e12 
 |-  (. A e. B ,. x e. { A } ->. x e. B ).
8 7 in2 
 |-  (. A e. B ->. ( x e. { A } -> x e. B ) ).
9 8 gen11 
 |-  (. A e. B ->. A. x ( x e. { A } -> x e. B ) ).
10 biimpr 
 |-  ( ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) ) -> ( A. x ( x e. { A } -> x e. B ) -> { A } C_ B ) )
11 1 9 10 e01 
 |-  (. A e. B ->. { A } C_ B ).
12 11 in1 
 |-  ( A e. B -> { A } C_ B )