Theorem relopabv 5777

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

Syntax hints:  {copab 5148  Rel wrel 5636

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5637  df-rel 5638

This theorem is referenced by:  opabid2  5784  inopab  5785  difopab  5786  dfres2  6007  cnvopab  6101  cnvopabOLD  6102  funopab  6534  elopabi  8015  relmpoopab  8044  shftfn  15035  cicer  17773  joindmss  18343  meetdmss  18357  lgsquadlem3  27345  tgjustf  28541  perpln1  28778  perpln2  28779  fpwrelmapffslem  32805  fpwrelmap  32806  relfae  34391  satfrel  35549  xpab  35908  vvdifopab  38586  inxprnres  38619  prtlem12  39313  dicvalrelN  41631  diclspsn  41640  dih1dimatlem  41775  rfovcnvf1od  44431