Theorem relopabv 5808

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

Syntax hints:  {copab 5172  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-opab 5173  df-xp 5667  df-rel 5668

This theorem is referenced by:  opabid2  5815  inopab  5816  difopab  5817  dfres2  6043  cnvopab  6137  funopab  6571  elopabi  8058  relmpoopab  8088  shftfn  15109  cicer  17862  joindmss  18432  meetdmss  18446  lgsquadlem3  27522  tgjustf  28718  perpln1  28965  perpln2  28966  fpwrelmapffslem  33043  fpwrelmap  33044  relfae  34603  satfrel  35813  xpab  36172  vvdifopab  38860  inxprnres  38893  prtlem12  39587  dicvalrelN  41905  diclspsn  41914  dih1dimatlem  42049  rfovcnvf1od  44678