Theorem elabreximd

Description: Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016)

	Ref	Expression
Hypotheses	elabreximd.1	⊢ Ⅎ 𝑥 𝜑
	elabreximd.2	⊢ Ⅎ 𝑥 𝜒
	elabreximd.3	⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
	elabreximd.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elabreximd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 )
Assertion	elabreximd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		elabreximd.1	⊢ Ⅎ 𝑥 𝜑
2		elabreximd.2	⊢ Ⅎ 𝑥 𝜒
3		elabreximd.3	⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
4		elabreximd.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		elabreximd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 )
6		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝐴 = 𝐵 ) )
7	6	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 ) )
8	7	elabg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 ) )
9	4 8	syl	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 ) )
10	9	biimpa	⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
12	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝜓 )
13	3	biimpar	⊢ ( ( 𝐴 = 𝐵 ∧ 𝜓 ) → 𝜒 )
14	11 12 13	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝐴 = 𝐵 ) → 𝜒 )
15	14	exp31	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 → ( 𝐴 = 𝐵 → 𝜒 ) ) )
16	1 2 15	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 → 𝜒 ) )
17	16	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐶 𝐴 = 𝐵 ) → 𝜒 )
18	10 17	syldan	⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 )