Theorem ismgmn0

Description: The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	ismgmn0.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ismgmn0.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	ismgmn0	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmn0.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		ismgmn0.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3	1	eleq2i	⊢ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ( Base ‘ 𝑀 ) )
4	3	biimpi	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ ( Base ‘ 𝑀 ) )
5	4	elfvexd	⊢ ( 𝐴 ∈ 𝐵 → 𝑀 ∈ V )
6	1 2	ismgm	⊢ ( 𝑀 ∈ V → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
7	5 6	syl	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )