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