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 A V A B A B

Proof

Step Hyp Ref Expression
1 velsn x A x = A
2 1 imbi1i x A x B x = A x B
3 2 albii x x A x B x x = A x B
4 3 a1i A V x x A x B x x = A x B
5 dfss2 A B x x A x B
6 5 a1i A V A B x x A x B
7 clel2g A V A B x x = A x B
8 4 6 7 3bitr4rd A V A B A B