Metamath Proof Explorer


Theorem relopabiv

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 and ax-12 , see relopabi . (Contributed by BJ, 22-Jul-2023)

Ref Expression
Hypothesis relopabiv.1 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion relopabiv Rel 𝐴

Proof

Step Hyp Ref Expression
1 relopabiv.1 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2 vex 𝑥 ∈ V
3 vex 𝑦 ∈ V
4 2 3 pm3.2i ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
5 4 a1i ( 𝜑 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) )
6 5 ssopab2i { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
7 df-xp ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
8 6 1 7 3sstr4i 𝐴 ⊆ ( V × V )
9 df-rel ( Rel 𝐴𝐴 ⊆ ( V × V ) )
10 8 9 mpbir Rel 𝐴