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 ( 𝑅𝐴 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑥 𝑅 𝑦 ) }