Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brel | Structured version Visualization version GIF version |
Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
brel.1 | ⊢ 𝑅 ⊆ (𝐶 × 𝐷) |
Ref | Expression |
---|---|
brel | ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brel.1 | . . 3 ⊢ 𝑅 ⊆ (𝐶 × 𝐷) | |
2 | 1 | ssbri 5120 | . 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵) |
3 | brxp 5637 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
4 | 2, 3 | sylib 217 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2107 ⊆ wss 3888 class class class wbr 5075 × cxp 5588 |
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 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-br 5076 df-opab 5138 df-xp 5596 |
This theorem is referenced by: brab2a 5681 soirri 6036 sotri 6037 sotri2 6039 sotri3 6040 ndmovord 7471 ndmovordi 7472 swoer 8537 brecop2 8609 ecopovsym 8617 ecopovtrn 8618 hartogslem1 9310 nlt1pi 10671 indpi 10672 nqerf 10695 ordpipq 10707 lterpq 10735 ltexnq 10740 ltbtwnnq 10743 ltrnq 10744 prnmadd 10762 genpcd 10771 nqpr 10779 1idpr 10794 ltexprlem4 10804 ltexpri 10808 ltaprlem 10809 prlem936 10812 reclem2pr 10813 reclem3pr 10814 reclem4pr 10815 suplem1pr 10817 suplem2pr 10818 supexpr 10819 recexsrlem 10868 addgt0sr 10869 mulgt0sr 10870 mappsrpr 10873 map2psrpr 10875 supsrlem 10876 supsr 10877 ltresr 10905 dfle2 12890 dflt2 12891 dvdszrcl 15977 letsr 18320 hmphtop 22938 brtxp2 34192 brpprod3a 34197 brxrn2 36512 iccdisj2 46202 i0oii 46224 io1ii 46225 |
Copyright terms: Public domain | W3C validator |