Theorem relopabv 5784

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 5787. (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 5783	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5169  Rel wrel 5643

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 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  opabid2  5791  inopab  5792  difopab  5793  difopabOLD  5794  dfres2  6012  cnvopab  6110  cnvopabOLD  6111  funopab  6551  elopabi  8041  relmpoopab  8073  shftfn  15039  cicer  17768  joindmss  18338  meetdmss  18352  lgsquadlem3  27293  tgjustf  28400  perpln1  28637  perpln2  28638  fpwrelmapffslem  32655  fpwrelmap  32656  relfae  34237  satfrel  35354  xpab  35713  vvdifopab  38249  inxprnres  38280  prtlem12  38860  dicvalrelN  41179  diclspsn  41188  dih1dimatlem  41323  rfovcnvf1od  43993