Theorem cdeqel

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

	Ref	Expression
Hypotheses	cdeqeq.1	⊢ CondEq ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	cdeqeq.2	⊢ CondEq ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion	cdeqel	⊢ CondEq ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cdeqeq.1	⊢ CondEq ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2		cdeqeq.2	⊢ CondEq ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
3	1	cdeqri	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
4	2	cdeqri	⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
5	3 4	eleq12d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷 ) )
6	5	cdeqi	⊢ CondEq ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷 ) )