![]() |
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 5408 | . . . . 5 ⊢ (Rel 𝑅 ↔ 𝑅 ⊆ (V × V)) | |
2 | 1 | biimpi 208 | . . . 4 ⊢ (Rel 𝑅 → 𝑅 ⊆ (V × V)) |
3 | 2 | ssbrd 4966 | . . 3 ⊢ (Rel 𝑅 → (𝐴𝑅𝐵 → 𝐴(V × V)𝐵)) |
4 | 3 | imp 398 | . 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴(V × V)𝐵) |
5 | brxp 5447 | . 2 ⊢ (𝐴(V × V)𝐵 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | |
6 | 4, 5 | sylib 210 | 1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 Vcvv 3409 ⊆ wss 3823 class class class wbr 4923 × cxp 5399 Rel wrel 5406 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pr 5180 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4924 df-opab 4986 df-xp 5407 df-rel 5408 |
This theorem is referenced by: brrelex1 5449 brrelex2 5450 brrelex12i 5451 relbrcnvg 5802 brovex 7685 ersym 8095 relelec 8128 fpwwe2lem2 9846 fpwwelem 9859 cofuval2 17009 isnat 17069 pslem 17668 frgpuplem 18652 perpln1 26192 perpln2 26193 poprelb 43054 |
Copyright terms: Public domain | W3C validator |