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 5076 | . 2 ⊢ (𝐴𝑅𝐵 → 𝐴(𝐶 × 𝐷)𝐵) |
3 | brxp 5573 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
4 | 2, 3 | sylib 221 | 1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2113 ⊆ wss 3844 class class class wbr 5031 × cxp 5524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3400 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 df-xp 5532 |
This theorem is referenced by: brab2a 5616 soirri 5961 sotri 5962 sotri2 5964 sotri3 5965 ndmovord 7355 ndmovordi 7356 swoer 8351 brecop2 8423 ecopovsym 8431 ecopovtrn 8432 hartogslem1 9080 nlt1pi 10407 indpi 10408 nqerf 10431 ordpipq 10443 lterpq 10471 ltexnq 10476 ltbtwnnq 10479 ltrnq 10480 prnmadd 10498 genpcd 10507 nqpr 10515 1idpr 10530 ltexprlem4 10540 ltexpri 10544 ltaprlem 10545 prlem936 10548 reclem2pr 10549 reclem3pr 10550 reclem4pr 10551 suplem1pr 10553 suplem2pr 10554 supexpr 10555 recexsrlem 10604 addgt0sr 10605 mulgt0sr 10606 mappsrpr 10609 map2psrpr 10611 supsrlem 10612 supsr 10613 ltresr 10641 dfle2 12624 dflt2 12625 dvdszrcl 15705 letsr 17954 hmphtop 22530 brtxp2 33821 brpprod3a 33826 brxrn2 36125 iccdisj2 45706 i0oii 45727 io1ii 45728 |
Copyright terms: Public domain | W3C validator |