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

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

Proof of Theorem brinxp2
StepHypRef Expression
1 brin 5115 . 2 (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ (𝐶𝑅𝐷𝐶(𝐴 × 𝐵)𝐷))
2 ancom 461 . 2 ((𝐶𝑅𝐷𝐶(𝐴 × 𝐵)𝐷) ↔ (𝐶(𝐴 × 𝐵)𝐷𝐶𝑅𝐷))
3 brxp 5600 . . 3 (𝐶(𝐴 × 𝐵)𝐷 ↔ (𝐶𝐴𝐷𝐵))
43anbi1i 623 . 2 ((𝐶(𝐴 × 𝐵)𝐷𝐶𝑅𝐷) ↔ ((𝐶𝐴𝐷𝐵) ∧ 𝐶𝑅𝐷))
51, 2, 43bitri 298 1 (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶𝐴𝐷𝐵) ∧ 𝐶𝑅𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wcel 2107  cin 3939   class class class wbr 5063   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560
This theorem is referenced by:  brinxp  5629  opelinxp  5630  fncnv  6424  erinxp  8361  fpwwe2lem8  10048  fpwwe2lem9  10049  fpwwe2lem12  10052  nqerf  10341  nqerid  10344  isstruct  16486  pwsle  16755  psss  17814  psssdm2  17815  pi1cpbl  23563  pi1grplem  23568  brres2  35397  inxpss  35437  inxpss3  35439  idinxpssinxp2  35443  inxp2  35486  inxpxrn  35510
  Copyright terms: Public domain W3C validator