Theorem relopabv 5668

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2158 and ax-12 2175, see relopab 5671. (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 2758	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5667	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5098  Rel wrel 5533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5099  df-xp 5534  df-rel 5535

This theorem is referenced by:  opabid2  5675  inopab  5676  difopab  5677  dfres2  5886  cnvopab  5974  funopab  6375  elopabi  7770  relmpoopab  7800  shftfn  14493  cicer  17149  joindmss  17697  meetdmss  17711  lgsquadlem3  26079  tgjustf  26380  perpln1  26617  perpln2  26618  fpwrelmapffslem  30604  fpwrelmap  30605  relfae  31747  satfrel  32858  xpab  33208  vvdifopab  35996  inxprnres  36024  prtlem12  36478  dicvalrelN  38796  diclspsn  38805  dih1dimatlem  38940  rfovcnvf1od  41123