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 syl5bb ( 𝐶𝑉 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅𝐴 ) ↔ ( 𝐵𝐴 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) )