![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brrelex12 | Structured version Visualization version GIF version |
Description: A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
brrelex12 | ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rel 5150 | . . . . 5 ⊢ (Rel 𝑅 ↔ 𝑅 ⊆ (V × V)) | |
2 | 1 | biimpi 206 | . . . 4 ⊢ (Rel 𝑅 → 𝑅 ⊆ (V × V)) |
3 | 2 | ssbrd 4728 | . . 3 ⊢ (Rel 𝑅 → (𝐴𝑅𝐵 → 𝐴(V × V)𝐵)) |
4 | 3 | imp 444 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴(V × V)𝐵) |
5 | brxp 5181 | . 2 ⊢ (𝐴(V × V)𝐵 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
6 | 4, 5 | sylib 208 | 1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2030 Vcvv 3231 ⊆ wss 3607 class class class wbr 4685 × cxp 5141 Rel wrel 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-xp 5149 df-rel 5150 |
This theorem is referenced by: brrelex 5190 brrelex2 5191 nprrel12 5194 relbrcnvg 5539 ovprc 6723 oprabv 6745 brovex 7393 ersym 7799 relelec 7830 encv 8005 fsuppunbi 8337 fpwwe2lem2 9492 fpwwelem 9505 brfi1uzind 13318 isstruct2 15914 brssc 16521 cofuval2 16594 isfull 16617 isfth 16621 isnat 16654 pslem 17253 frgpuplem 18231 dvdsr 18692 ulmval 24179 perpln1 25650 perpln2 25651 opelco3 31802 rngoablo2 33838 aovprc 41589 aovrcl 41590 nelbrim 41616 |
Copyright terms: Public domain | W3C validator |