![]() |
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 2155 and ax-12 2172, see relopab 5825. (Contributed by SN, 8-Sep-2024.) |
Ref | Expression |
---|---|
relopabv | ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2733 | . 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑} | |
2 | 1 | relopabiv 5821 | 1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: {copab 5211 Rel wrel 5682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-opab 5212 df-xp 5683 df-rel 5684 |
This theorem is referenced by: opabid2 5829 inopab 5830 difopab 5831 difopabOLD 5832 dfres2 6042 cnvopab 6139 funopab 6584 elopabi 8048 relmpoopab 8080 shftfn 15020 cicer 17753 joindmss 18332 meetdmss 18346 lgsquadlem3 26885 tgjustf 27724 perpln1 27961 perpln2 27962 fpwrelmapffslem 31957 fpwrelmap 31958 relfae 33245 satfrel 34358 xpab 34695 vvdifopab 37128 inxprnres 37161 prtlem12 37737 dicvalrelN 40056 diclspsn 40065 dih1dimatlem 40200 rfovcnvf1od 42755 |
Copyright terms: Public domain | W3C validator |