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	|- B e. C
Assertion	elimel	|- if ( A e. C , A , B ) e. C

Proof

Step	Hyp	Ref	Expression
1		elimel.1	|- B e. C
2		eleq1	|- ( A = if ( A e. C , A , B ) -> ( A e. C <-> if ( A e. C , A , B ) e. C ) )
3		eleq1	|- ( B = if ( A e. C , A , B ) -> ( B e. C <-> if ( A e. C , A , B ) e. C ) )
4	2 3 1	elimhyp	|- if ( A e. C , A , B ) e. C