Theorem relopabv 5795

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 5798. (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 2760	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5794	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

This proof depends on syntax axioms:  {copab 5166  Rel wrel 5652

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-opab 5167  df-xp 5653  df-rel 5654

This theorem is used by:  opabid2  5802  inopab  5803  difopab  5804  dfres2  6031  cnvopab  6125  funopab  6563  elopabi  8056  relmpoopab  8088  shftfn  15194  cicer  17943  joindmss  18513  meetdmss  18527  lgsquadlem3  27673  tgjustf  28869  perpln1  29119  perpln2  29120  fpwrelmapffslem  33258  fpwrelmap  33259  relfae  34814  satfrel  36053  xpab  36412  vvdifopab  39117  inxprnres  39150  prtlem12  39844  dicvalrelN  42162  diclspsn  42171  dih1dimatlem  42306  rfovcnvf1od  44948