Theorem elimasng1

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006) Revise to use df-br and to prove elimasn1 from it. (Revised by BJ, 16-Oct-2024)

	Ref	Expression
Assertion	elimasng1	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → 𝐶 ∈ 𝑊 )
2		imasng	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 “ { 𝐵 } ) = { 𝑥 ∣ 𝐵 𝐴 𝑥 } )
3	2	adantr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐴 “ { 𝐵 } ) = { 𝑥 ∣ 𝐵 𝐴 𝑥 } )
4		simpr	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 = 𝐶 ) → 𝑥 = 𝐶 )
5	4	breq2d	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) ∧ 𝑥 = 𝐶 ) → ( 𝐵 𝐴 𝑥 ↔ 𝐵 𝐴 𝐶 ) )
6	1 3 5	elabd2	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )