Theorem symgbasexOLD

Description: Obsolete as of 8-Aug-2024. B e. _V follows immediatly from fvex . (Contributed by AV, 30-Mar-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	symgbas.1	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgbasexOLD	|- ( A e. V -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	symgbas	|- B = { f | f : A -1-1-onto-> A }
4		permsetexOLD	|- ( A e. V -> { f | f : A -1-1-onto-> A } e. _V )
5	3 4	eqeltrid	|- ( A e. V -> B e. _V )