Theorem relopabv 5783

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

Syntax hints:  {copab 5152  Rel wrel 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-ss 3912  df-opab 5153  df-xp 5642  df-rel 5643

This theorem is referenced by:  opabid2  5790  inopab  5791  difopab  5792  dfres2  6016  cnvopab  6110  funopab  6541  elopabi  8028  relmpoopab  8057  shftfn  15072  cicer  17811  joindmss  18381  meetdmss  18395  lgsquadlem3  27412  tgjustf  28608  perpln1  28845  perpln2  28846  fpwrelmapffslem  32873  fpwrelmap  32874  relfae  34488  satfrel  35655  xpab  36014  vvdifopab  38702  inxprnres  38735  prtlem12  39429  dicvalrelN  41747  diclspsn  41756  dih1dimatlem  41891  rfovcnvf1od  44518