Theorem elrng

Description: Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	elrng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elrn2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 ) )
2		df-br	⊢ ( 𝑥 𝐵 𝐴 ↔ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 )
3	2	exbii	⊢ ( ∃ 𝑥 𝑥 𝐵 𝐴 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 )
4	1 3	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝐴 ) )