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

Metamath Proof Explorer

Theorem opelres

Description: Ordered pair elementhood in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995) (Revised by BJ, 18-Feb-2022) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

Ref Expression
Assertion opelres ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × V ) )
2 1 elin2 ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 ↾ 𝐴 ) ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × V ) ) )
3 opelxp ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × V ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
4 elex ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
5 4 biantrud ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐵 ∈ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ V ) ) )
6 3 5 bitr4id ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × V ) ↔ 𝐵 ∈ 𝐴 ) )
7 6 anbi1cd ⊢ ( 𝐶 ∈ 𝑉 → ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝐴 × V ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )
8 2 7 bitrid ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )