Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > relopabiv | Structured version Visualization version GIF version |
Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2158 and ax-12 2175, see relopabi 5681. (Contributed by BJ, 22-Jul-2023.) |
Ref | Expression |
---|---|
relopabiv.1 | ⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} |
Ref | Expression |
---|---|
relopabiv | ⊢ Rel 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3405 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | vex 3405 | . . . . . 6 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | pm3.2i 474 | . . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V) |
4 | 3 | a1i 11 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V)) |
5 | 4 | ssopab2i 5420 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} |
6 | relopabiv.1 | . . 3 ⊢ 𝐴 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
7 | df-xp 5546 | . . 3 ⊢ (V × V) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} | |
8 | 5, 6, 7 | 3sstr4i 3934 | . 2 ⊢ 𝐴 ⊆ (V × V) |
9 | df-rel 5547 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
10 | 8, 9 | mpbir 234 | 1 ⊢ Rel 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1543 ∈ wcel 2110 Vcvv 3401 ⊆ wss 3857 {copab 5105 × cxp 5538 Rel wrel 5545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2706 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2713 df-cleq 2726 df-clel 2812 df-v 3403 df-in 3864 df-ss 3874 df-opab 5106 df-xp 5546 df-rel 5547 |
This theorem is referenced by: relopabv 5680 mptrel 5684 reli 5685 rele 5686 relcnv 5961 cotrg 5965 relco 6097 brfvopabrbr 6804 reloprab 7259 reldmoprab 7305 relrpss 7501 eqer 8415 ecopover 8492 relen 8620 reldom 8621 relfsupp 8976 relwdom 9171 fpwwe2lem2 10229 fpwwe2lem3 10230 fpwwe2lem5 10232 fpwwe2lem6 10233 fpwwe2lem8 10235 fpwwe2lem10 10237 fpwwe2lem11 10238 fpwwe2lem12 10239 fpwwelem 10242 climrel 15036 rlimrel 15037 brstruct 16693 sscrel 17290 gaorber 18674 sylow2a 18980 efgrelexlemb 19112 efgcpbllemb 19117 rellindf 20742 psrbaglesupp 20855 2ndcctbss 22324 refrel 22377 vitalilem1 24477 lgsquadlem1 26233 lgsquadlem2 26234 relsubgr 27329 vcrel 28613 h2hlm 29033 hlimi 29241 relfldext 31407 relmntop 31658 relae 31892 dmscut 33699 fnerel 34221 filnetlem3 34263 brabg2 35568 heiborlem3 35665 heiborlem4 35666 relrngo 35748 isdivrngo 35802 drngoi 35803 isdrngo1 35808 riscer 35840 relcoss 36240 relssr 36312 prter1 36587 prter3 36590 prjsper 40107 reldvds 41558 nelbrim 44393 isomgrrel 44901 rellininds 45411 |
Copyright terms: Public domain | W3C validator |