Theorem caovass

Description: Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

	Ref	Expression
Hypotheses	caovass.1	⊢ 𝐴 ∈ V
	caovass.2	⊢ 𝐵 ∈ V
	caovass.3	⊢ 𝐶 ∈ V
	caovass.4	⊢ ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
Assertion	caovass	⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		caovass.1	⊢ 𝐴 ∈ V
2		caovass.2	⊢ 𝐵 ∈ V
3		caovass.3	⊢ 𝐶 ∈ V
4		caovass.4	⊢ ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
5		tru	⊢ ⊤
6	4	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) ) → ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) ) )
7	6	caovassg	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) )
8	5 7	mpan	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) ) )
9	1 2 3 8	mp3an	⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐹 𝐶 ) = ( 𝐴 𝐹 ( 𝐵 𝐹 𝐶 ) )