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

Metamath Proof Explorer

Theorem elres

Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022)

Ref Expression
Assertion elres ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
2 1 eleq2i ⊢ ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ 𝐴 ∈ ( 𝐵 ∩ ( 𝐶 × V ) ) )
3 elinxp ⊢ ( 𝐴 ∈ ( 𝐵 ∩ ( 𝐶 × V ) ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
4 rexv ⊢ ( ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
5 4 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
6 2 3 5 3bitri ⊢ ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )