This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ( 𝐵 ↾ { 𝐶 } ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝐶 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐵 ) )