Theorem relopabv 5775

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

Syntax hints:  {copab 5164  Rel wrel 5636

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  opabid2  5782  inopab  5783  difopab  5784  dfres2  6001  cnvopab  6098  cnvopabOLD  6099  funopab  6535  elopabi  8020  relmpoopab  8050  shftfn  15016  cicer  17749  joindmss  18319  meetdmss  18333  lgsquadlem3  27327  tgjustf  28454  perpln1  28691  perpln2  28692  fpwrelmapffslem  32706  fpwrelmap  32707  relfae  34231  satfrel  35348  xpab  35707  vvdifopab  38243  inxprnres  38274  prtlem12  38854  dicvalrelN  41173  diclspsn  41182  dih1dimatlem  41317  rfovcnvf1od  43987