![]() |
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 5193 | . 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵) |
3 | brxp 5725 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
4 | 2, 3 | sylib 217 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ⊆ wss 3948 class class class wbr 5148 × cxp 5674 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 |
This theorem is referenced by: brab2a 5769 soirri 6127 sotri 6128 sotri2 6130 sotri3 6131 ndmovord 7599 ndmovordi 7600 swoer 8735 brecop2 8807 ecopovsym 8815 ecopovtrn 8816 hartogslem1 9539 nlt1pi 10903 indpi 10904 nqerf 10927 ordpipq 10939 lterpq 10967 ltexnq 10972 ltbtwnnq 10975 ltrnq 10976 prnmadd 10994 genpcd 11003 nqpr 11011 1idpr 11026 ltexprlem4 11036 ltexpri 11040 ltaprlem 11041 prlem936 11044 reclem2pr 11045 reclem3pr 11046 reclem4pr 11047 suplem1pr 11049 suplem2pr 11050 supexpr 11051 recexsrlem 11100 addgt0sr 11101 mulgt0sr 11102 mappsrpr 11105 map2psrpr 11107 supsrlem 11108 supsr 11109 ltresr 11137 dfle2 13128 dflt2 13129 dvdszrcl 16204 letsr 18548 hmphtop 23289 brtxp2 34928 brpprod3a 34933 brxrn2 37337 iccdisj2 47614 i0oii 47636 io1ii 47637 |
Copyright terms: Public domain | W3C validator |