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

Metamath Proof Explorer

Theorem inxprnres

Description: Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion inxprnres ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }

Proof

Step Hyp Ref Expression
1 relinxp ⊢ Rel ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) )
2 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }
3 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
4 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) )
5 3 4 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) )
6 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑤 ) )
7 6 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) )
8 5 7 opelopabg ⊢ ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) )
9 8 el2v ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) )
10 brinxprnres ⊢ ( 𝑤 ∈ V → ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) ) )
11 10 elv ⊢ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑤 ) )
12 df-br ⊢ ( 𝑧 ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) )
13 9 11 12 3bitr2ri ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } )
14 1 2 13 eqrelriiv ⊢ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }