Theorem asslawass

Description: Associativity of an associative operation. (Contributed by FL, 2-Nov-2009) (Revised by AV, 21-Jan-2020)

	Ref	Expression
Assertion	asslawass	⊢ ( ⚬ assLaw 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-asslaw	⊢ assLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ∀ 𝑧 ∈ 𝑚 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }
2	1	bropaex12	⊢ ( ⚬ assLaw 𝑀 → ( ⚬ ∈ V ∧ 𝑀 ∈ V ) )
3		isasslaw	⊢ ( ( ⚬ ∈ V ∧ 𝑀 ∈ V ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
4	2 3	syl	⊢ ( ⚬ assLaw 𝑀 → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
5	4	ibi	⊢ ( ⚬ assLaw 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )