Theorem elrelimasn

Description: Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015)

	Ref	Expression
Assertion	elrelimasn	⊢ ( Rel 𝑅 → ( 𝐵 ∈ ( 𝑅 “ { 𝐴 } ) ↔ 𝐴 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		relimasn	⊢ ( Rel 𝑅 → ( 𝑅 “ { 𝐴 } ) = { 𝑥 ∣ 𝐴 𝑅 𝑥 } )
2	1	eleq2d	⊢ ( Rel 𝑅 → ( 𝐵 ∈ ( 𝑅 “ { 𝐴 } ) ↔ 𝐵 ∈ { 𝑥 ∣ 𝐴 𝑅 𝑥 } ) )
3		brrelex2	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 ∈ V )
4	3	ex	⊢ ( Rel 𝑅 → ( 𝐴 𝑅 𝐵 → 𝐵 ∈ V ) )
5		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥 ↔ 𝐴 𝑅 𝐵 ) )
6	5	elab3g	⊢ ( ( 𝐴 𝑅 𝐵 → 𝐵 ∈ V ) → ( 𝐵 ∈ { 𝑥 ∣ 𝐴 𝑅 𝑥 } ↔ 𝐴 𝑅 𝐵 ) )
7	4 6	syl	⊢ ( Rel 𝑅 → ( 𝐵 ∈ { 𝑥 ∣ 𝐴 𝑅 𝑥 } ↔ 𝐴 𝑅 𝐵 ) )
8	2 7	bitrd	⊢ ( Rel 𝑅 → ( 𝐵 ∈ ( 𝑅 “ { 𝐴 } ) ↔ 𝐴 𝑅 𝐵 ) )