Theorem relopabv 5787

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 2178, see relopab 5790. (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 2730	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5786	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5172  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  opabid2  5794  inopab  5795  difopab  5796  difopabOLD  5797  dfres2  6015  cnvopab  6113  cnvopabOLD  6114  funopab  6554  elopabi  8044  relmpoopab  8076  shftfn  15046  cicer  17775  joindmss  18345  meetdmss  18359  lgsquadlem3  27300  tgjustf  28407  perpln1  28644  perpln2  28645  fpwrelmapffslem  32662  fpwrelmap  32663  relfae  34244  satfrel  35361  xpab  35720  vvdifopab  38256  inxprnres  38287  prtlem12  38867  dicvalrelN  41186  diclspsn  41195  dih1dimatlem  41330  rfovcnvf1od  44000