Theorem cdeqel

Description: Distribute conditional equality over elementhood. (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Hypotheses	cdeqeq.1	|- CondEq ( x = y -> A = B )
	cdeqeq.2	|- CondEq ( x = y -> C = D )
Assertion	cdeqel	|- CondEq ( x = y -> ( A e. C <-> B e. D ) )

Proof

Step	Hyp	Ref	Expression
1		cdeqeq.1	|- CondEq ( x = y -> A = B )
2		cdeqeq.2	|- CondEq ( x = y -> C = D )
3	1	cdeqri	|- ( x = y -> A = B )
4	2	cdeqri	|- ( x = y -> C = D )
5	3 4	eleq12d	|- ( x = y -> ( A e. C <-> B e. D ) )
6	5	cdeqi	|- CondEq ( x = y -> ( A e. C <-> B e. D ) )