Theorem relopab 5698

Description: A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) Remove disjoint variable conditions. (Revised by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)

Assertion

Ref	Expression
relopab	⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem relopab

Step	Hyp	Ref	Expression
1		eqid 2823	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabi 5696	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5130  Rel wrel 5562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-opab 5131  df-xp 5563  df-rel 5564

This theorem is referenced by:  opabid2  5702  inopab  5703  difopab  5704  dfres2  5911  cnvopab  5999  funopab  6392  relmptopab  7397  elopabi  7762  relmpoopab  7791  shftfn  14434  cicer  17078  joindmss  17619  meetdmss  17633  lgsquadlem3  25960  tgjustf  26261  perpln1  26498  perpln2  26499  fpwrelmapffslem  30470  fpwrelmap  30471  relfae  31508  satfrel  32616  bj-0nelopab  34360  vvdifopab  35523  inxprnres  35551  prtlem12  36005  dicvalrelN  38323  diclspsn  38332  dih1dimatlem  38467  rfovcnvf1od  40357