![]() |
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 2155 and ax-12 2172, see relopabi 5783. (Contributed by BJ, 22-Jul-2023.) |
Ref | Expression |
---|---|
relopabiv.1 | ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
Ref | Expression |
---|---|
relopabiv | ⊢ Rel 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3452 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | vex 3452 | . . . . . 6 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | pm3.2i 472 | . . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V) |
4 | 3 | a1i 11 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V)) |
5 | 4 | ssopab2i 5512 | . . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} |
6 | relopabiv.1 | . . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} | |
7 | df-xp 5644 | . . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} | |
8 | 5, 6, 7 | 3sstr4i 3992 | . 2 ⊢ 𝐴 ⊆ (V × V) |
9 | df-rel 5645 | . 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | |
10 | 8, 9 | mpbir 230 | 1 ⊢ Rel 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∈ wcel 2107 Vcvv 3448 ⊆ wss 3915 {copab 5172 × cxp 5636 Rel wrel 5643 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-opab 5173 df-xp 5644 df-rel 5645 |
This theorem is referenced by: relopabv 5782 mptrel 5786 reli 5787 rele 5788 relcnv 6061 relco 6065 brfvopabrbr 6950 reloprab 7421 reldmoprab 7467 relrpss 7666 eqer 8690 ecopover 8767 relen 8895 reldom 8896 relfsupp 9314 relwdom 9509 fpwwe2lem2 10575 fpwwe2lem3 10576 fpwwe2lem5 10578 fpwwe2lem6 10579 fpwwe2lem8 10581 fpwwe2lem10 10583 fpwwe2lem11 10584 fpwwe2lem12 10585 fpwwelem 10588 climrel 15381 rlimrel 15382 brstruct 17027 sscrel 17703 gaorber 19095 sylow2a 19408 efgrelexlemb 19539 efgcpbllemb 19544 rellindf 21230 psrbaglesupp 21342 2ndcctbss 22822 refrel 22875 vitalilem1 24988 lgsquadlem1 26744 lgsquadlem2 26745 dmscut 27172 relsubgr 28259 vcrel 29544 h2hlm 29964 hlimi 30172 relfldext 32375 relmntop 32645 relae 32879 fnerel 34839 filnetlem3 34881 brabg2 36204 heiborlem3 36301 heiborlem4 36302 relrngo 36384 isdivrngo 36438 drngoi 36439 isdrngo1 36444 riscer 36476 relcoss 36914 relssr 36991 prter1 37370 prter3 37373 prjsper 40975 reldvds 42669 nelbrim 45581 isomgrrel 46088 rellininds 46598 |
Copyright terms: Public domain | W3C validator |