MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brinxp2 Structured version   Visualization version   GIF version

Theorem brinxp2 5762
Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.) Group conjuncts and avoid df-3an 1088. (Revised by Peter Mazsa, 18-Sep-2022.)
Assertion
Ref Expression
brinxp2 (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶𝐴𝐷𝐵) ∧ 𝐶𝑅𝐷))

Proof of Theorem brinxp2
StepHypRef Expression
1 brin 5194 . 2 (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ (𝐶𝑅𝐷𝐶(𝐴 × 𝐵)𝐷))
2 ancom 460 . 2 ((𝐶𝑅𝐷𝐶(𝐴 × 𝐵)𝐷) ↔ (𝐶(𝐴 × 𝐵)𝐷𝐶𝑅𝐷))
3 brxp 5733 . . 3 (𝐶(𝐴 × 𝐵)𝐷 ↔ (𝐶𝐴𝐷𝐵))
43anbi1i 624 . 2 ((𝐶(𝐴 × 𝐵)𝐷𝐶𝑅𝐷) ↔ ((𝐶𝐴𝐷𝐵) ∧ 𝐶𝑅𝐷))
51, 2, 43bitri 297 1 (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶𝐴𝐷𝐵) ∧ 𝐶𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2107  cin 3949   class class class wbr 5142   × cxp 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690
This theorem is referenced by:  brinxp  5763  opelinxp  5764  fncnv  6638  erinxp  8832  fpwwe2lem7  10678  fpwwe2lem8  10679  fpwwe2lem11  10682  nqerf  10971  nqerid  10974  isstruct  17190  pwsle  17538  psss  18626  psssdm2  18627  pi1cpbl  25078  pi1grplem  25083  br1cnvinxp  38258  brres2  38270  inxpss  38313  inxpss3  38316  idinxpssinxp2  38320  inxp2  38369  inxpxrn  38397
  Copyright terms: Public domain W3C validator