![]() |
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 5186 | . 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵) |
3 | brxp 5717 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
4 | 2, 3 | sylib 217 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ⊆ wss 3944 class class class wbr 5141 × cxp 5667 |
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 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
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 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-xp 5675 |
This theorem is referenced by: brab2a 5761 soirri 6116 sotri 6117 sotri2 6119 sotri3 6120 ndmovord 7580 ndmovordi 7581 swoer 8716 brecop2 8788 ecopovsym 8796 ecopovtrn 8797 hartogslem1 9519 nlt1pi 10883 indpi 10884 nqerf 10907 ordpipq 10919 lterpq 10947 ltexnq 10952 ltbtwnnq 10955 ltrnq 10956 prnmadd 10974 genpcd 10983 nqpr 10991 1idpr 11006 ltexprlem4 11016 ltexpri 11020 ltaprlem 11021 prlem936 11024 reclem2pr 11025 reclem3pr 11026 reclem4pr 11027 suplem1pr 11029 suplem2pr 11030 supexpr 11031 recexsrlem 11080 addgt0sr 11081 mulgt0sr 11082 mappsrpr 11085 map2psrpr 11087 supsrlem 11088 supsr 11089 ltresr 11117 dfle2 13108 dflt2 13109 dvdszrcl 16184 letsr 18528 hmphtop 23211 brtxp2 34683 brpprod3a 34688 brxrn2 37050 iccdisj2 47178 i0oii 47200 io1ii 47201 |
Copyright terms: Public domain | W3C validator |