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

Metamath Proof Explorer


Theorem prtlem12

Description: Lemma for prtex and prter3 . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion prtlem12 ( = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) } → Rel )

Proof

Step Hyp Ref Expression
1 relopabv Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) }
2 releq ( = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) } → ( Rel ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) } ) )
3 1 2 mpbiri ( = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝐴 ( 𝑥𝑢𝑦𝑢 ) } → Rel )