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=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbasexOLD	$$⊢A\in V\to B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
4		permsetexOLD	$$⊢A\in V\to \left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}$$
5	3 4	eqeltrid	$$⊢A\in V\to B\in \mathrm{V}$$