Theorem aevdemo

Description: Proof illustrating the comment of aev2 . (Contributed by BJ, 30-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	aevdemo	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑎 ∀ 𝑏 𝑐 = 𝑑 ∨ ∃ 𝑒 𝑓 = 𝑔 ) ∧ ∀ ℎ ( 𝑖 = 𝑗 → 𝑘 = 𝑙 ) ) )

Proof

Step	Hyp	Ref	Expression
1		aev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑒 𝑓 = 𝑔 )
2	1	19.2d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑒 𝑓 = 𝑔 )
3	2	olcd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑎 ∀ 𝑏 𝑐 = 𝑑 ∨ ∃ 𝑒 𝑓 = 𝑔 ) )
4		aev	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑚 𝑚 = 𝑛 )
5		aeveq	⊢ ( ∀ 𝑚 𝑚 = 𝑛 → 𝑘 = 𝑙 )
6	5	a1d	⊢ ( ∀ 𝑚 𝑚 = 𝑛 → ( 𝑖 = 𝑗 → 𝑘 = 𝑙 ) )
7	6	alrimiv	⊢ ( ∀ 𝑚 𝑚 = 𝑛 → ∀ ℎ ( 𝑖 = 𝑗 → 𝑘 = 𝑙 ) )
8	4 7	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ ℎ ( 𝑖 = 𝑗 → 𝑘 = 𝑙 ) )
9	3 8	jca	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑎 ∀ 𝑏 𝑐 = 𝑑 ∨ ∃ 𝑒 𝑓 = 𝑔 ) ∧ ∀ ℎ ( 𝑖 = 𝑗 → 𝑘 = 𝑙 ) ) )