Theorem elsnres

Description: Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011)

	Ref	Expression
Hypothesis	elsnres.1	⊢ 𝐶 ∈ V
Assertion	elsnres	⊢ ( 𝐴 ∈ ( 𝐵 ↾ { 𝐶 } ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elsnres.1	⊢ 𝐶 ∈ V
2		elres	⊢ ( 𝐴 ∈ ( 𝐵 ↾ { 𝐶 } ) ↔ ∃ 𝑥 ∈ { 𝐶 } ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3		rexcom4	⊢ ( ∃ 𝑥 ∈ { 𝐶 } ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑥 ∈ { 𝐶 } ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
4		opeq1	⊢ ( 𝑥 = 𝐶 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝑦 ⟩ )
5	4	eqeq2d	⊢ ( 𝑥 = 𝐶 → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ) )
6	4	eleq1d	⊢ ( 𝑥 = 𝐶 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )
7	5 6	anbi12d	⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) ) )
8	1 7	rexsn	⊢ ( ∃ 𝑥 ∈ { 𝐶 } ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ { 𝐶 } ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )
10	2 3 9	3bitri	⊢ ( 𝐴 ∈ ( 𝐵 ↾ { 𝐶 } ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )