Theorem elimasng

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006)

	Ref	Expression
Assertion	elimasng	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑦 = 𝐵 → { 𝑦 } = { 𝐵 } )
2	1	imaeq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 “ { 𝑦 } ) = ( 𝐴 “ { 𝐵 } ) )
3	2	eleq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↔ 𝑧 ∈ ( 𝐴 “ { 𝐵 } ) ) )
4		opeq1	⊢ ( 𝑦 = 𝐵 → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝑧 ⟩ )
5	4	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝐴 ) )
6	3 5	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) ↔ ( 𝑧 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝐴 ) ) )
7		eleq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ) )
8		opeq2	⊢ ( 𝑧 = 𝐶 → ⟨ 𝐵 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
9	8	eleq1d	⊢ ( 𝑧 = 𝐶 → ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) )
10	7 9	bibi12d	⊢ ( 𝑧 = 𝐶 → ( ( 𝑧 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝐴 ) ↔ ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) ) )
11		vex	⊢ 𝑦 ∈ V
12		vex	⊢ 𝑧 ∈ V
13	11 12	elimasn	⊢ ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
14	6 10 13	vtocl2g	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐴 ) )