Theorem brinxp2 5696

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 1094. (Revised by Peter Mazsa, 18-Sep-2022.)

Assertion

Ref	Expression
brinxp2	⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷))

Proof of Theorem brinxp2

Step	Hyp	Ref	Expression
1		brin 5124	. 2 ⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ (𝐶𝑅𝐷 ∧ 𝐶(𝐴 × 𝐵)𝐷))
2		ancom 461	. 2 ⊢ ((𝐶𝑅𝐷 ∧ 𝐶(𝐴 × 𝐵)𝐷) ↔ (𝐶(𝐴 × 𝐵)𝐷 ∧ 𝐶𝑅𝐷))
3		brxp 5667	. . 3 ⊢ (𝐶(𝐴 × 𝐵)𝐷 ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵))
4	3	anbi1i 630	. 2 ⊢ ((𝐶(𝐴 × 𝐵)𝐷 ∧ 𝐶𝑅𝐷) ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷))
5	1, 2, 4	3bitri 298	1 ⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   ∩ cin 3882   class class class wbr 5072   × cxp 5616

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624

This theorem is referenced by:  brinxp  5697  opelinxp  5698  fncnv  6558  erinxp  8728  fpwwe2lem7  10551  fpwwe2lem8  10552  fpwwe2lem11  10555  nqerf  10844  nqerid  10847  isstruct  17113  pwsle  17447  psss  18537  psssdm2  18538  pi1cpbl  25029  pi1grplem  25034  br1cnvinxp  38626  brres2  38640  inxpss  38684  inxpss3  38687  idinxpssinxp2  38691  inxp2  38742  inxpxrn  38785