Theorem elrnres

Description: Element of the range of a restriction. (Contributed by Peter Mazsa, 26-Dec-2018)

	Ref	Expression
Assertion	elrnres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ran ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elrng	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ran ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 𝑥 ( 𝑅 ↾ 𝐴 ) 𝐵 ) )
2		brres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ( 𝑅 ↾ 𝐴 ) 𝐵 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) )
3	2	exbidv	⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑥 𝑥 ( 𝑅 ↾ 𝐴 ) 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) )
4	1 3	bitrd	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ran ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) )
5		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) )
6	4 5	bitr4di	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ ran ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) )