Theorem relopabv 5799

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2194 and ax-12 2213, see relopab 5802. (Contributed by SN, 8-Sep-2024.)

Assertion

Ref	Expression
relopabv	⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem relopabv

Step	Hyp	Ref	Expression
1		eqid 2761	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5798	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

This proof depends on syntax axioms:  {copab 5167  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3915  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  opabid2  5806  inopab  5807  difopab  5808  dfres2  6033  cnvopab  6131  funopab  6576  elopabi  8074  relmpoopab  8106  shftfn  15227  cicer  17982  joindmss  18552  meetdmss  18566  lgsquadlem3  27710  tgjustf  28936  perpln1  29186  perpln2  29187  fpwrelmapffslem  33325  fpwrelmap  33326  relfae  34881  satfrel  36133  xpab  36492  vvdifopab  39199  inxprnres  39232  prtlem12  39926  dicvalrelN  42244  diclspsn  42253  dih1dimatlem  42388  rfovcnvf1od  45005