Theorem relelrnb

Description: Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015)

	Ref	Expression
Assertion	relelrnb	⊢ ( Rel 𝑅 → ( 𝐴 ∈ ran 𝑅 ↔ ∃ 𝑥 𝑥 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elrng	⊢ ( 𝐴 ∈ ran 𝑅 → ( 𝐴 ∈ ran 𝑅 ↔ ∃ 𝑥 𝑥 𝑅 𝐴 ) )
2	1	ibi	⊢ ( 𝐴 ∈ ran 𝑅 → ∃ 𝑥 𝑥 𝑅 𝐴 )
3		relelrn	⊢ ( ( Rel 𝑅 ∧ 𝑥 𝑅 𝐴 ) → 𝐴 ∈ ran 𝑅 )
4	3	ex	⊢ ( Rel 𝑅 → ( 𝑥 𝑅 𝐴 → 𝐴 ∈ ran 𝑅 ) )
5	4	exlimdv	⊢ ( Rel 𝑅 → ( ∃ 𝑥 𝑥 𝑅 𝐴 → 𝐴 ∈ ran 𝑅 ) )
6	2 5	impbid2	⊢ ( Rel 𝑅 → ( 𝐴 ∈ ran 𝑅 ↔ ∃ 𝑥 𝑥 𝑅 𝐴 ) )