Theorem caovdi

Description: Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 28-Jun-2013)

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

Proof

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