Theorem relopabv 5798

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2193 and ax-12 2212, see relopab 5801. (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 5797	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  opabid2  5805  inopab  5806  difopab  5807  dfres2  6032  cnvopab  6130  funopab  6575  elopabi  8073  relmpoopab  8105  shftfn  15227  cicer  17982  joindmss  18552  meetdmss  18566  lgsquadlem3  27710  tgjustf  28936  perpln1  29186  perpln2  29187  fpwrelmapffslem  33367  fpwrelmap  33368  relfae  34923  satfrel  36201  xpab  36566  vvdifopab  39273  inxprnres  39306  prtlem12  40000  dicvalrelN  42318  diclspsn  42327  dih1dimatlem  42462  rfovcnvf1od  45080