|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > relopabv | Structured version Visualization version GIF version | ||
| Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2156 and ax-12 2176, see relopab 5833. (Contributed by SN, 8-Sep-2024.) | 
| Ref | Expression | 
|---|---|
| relopabv | ⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqid 2736 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
| 2 | 1 | relopabiv 5829 | 1 ⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | 
| Colors of variables: wff setvar class | 
| Syntax hints: {copab 5204 Rel wrel 5689 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-ss 3967 df-opab 5205 df-xp 5690 df-rel 5691 | 
| This theorem is referenced by: opabid2 5837 inopab 5838 difopab 5839 difopabOLD 5840 dfres2 6058 cnvopab 6156 cnvopabOLD 6157 funopab 6600 elopabi 8088 relmpoopab 8120 shftfn 15113 cicer 17851 joindmss 18425 meetdmss 18439 lgsquadlem3 27427 tgjustf 28482 perpln1 28719 perpln2 28720 fpwrelmapffslem 32744 fpwrelmap 32745 relfae 34249 satfrel 35373 xpab 35727 vvdifopab 38262 inxprnres 38294 prtlem12 38869 dicvalrelN 41188 diclspsn 41197 dih1dimatlem 41332 rfovcnvf1od 44022 | 
| Copyright terms: Public domain | W3C validator |