Theorem elimel

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case B e. C is provable. (Contributed by NM, 15-May-1999)

	Ref	Expression
Hypothesis	elimel.1	⊢ 𝐵 ∈ 𝐶
Assertion	elimel	⊢ if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) ∈ 𝐶

Proof

Step	Hyp	Ref	Expression
1		elimel.1	⊢ 𝐵 ∈ 𝐶
2		eleq1	⊢ ( 𝐴 = if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) → ( 𝐴 ∈ 𝐶 ↔ if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) ∈ 𝐶 ) )
3		eleq1	⊢ ( 𝐵 = if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) → ( 𝐵 ∈ 𝐶 ↔ if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) ∈ 𝐶 ) )
4	2 3 1	elimhyp	⊢ if ( 𝐴 ∈ 𝐶 , 𝐴 , 𝐵 ) ∈ 𝐶