Theorem brinxp2 5701

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

Step	Hyp	Ref	Expression
1		brin 5147	. 2 ⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ (𝐶𝑅𝐷 ∧ 𝐶(𝐴 × 𝐵)𝐷))
2		ancom 460	. 2 ⊢ ((𝐶𝑅𝐷 ∧ 𝐶(𝐴 × 𝐵)𝐷) ↔ (𝐶(𝐴 × 𝐵)𝐷 ∧ 𝐶𝑅𝐷))
3		brxp 5672	. . 3 ⊢ (𝐶(𝐴 × 𝐵)𝐷 ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵))
4	3	anbi1i 624	. 2 ⊢ ((𝐶(𝐴 × 𝐵)𝐷 ∧ 𝐶𝑅𝐷) ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷))
5	1, 2, 4	3bitri 297	1 ⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ∩ cin 3904   class class class wbr 5095   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629

This theorem is referenced by:  brinxp  5702  opelinxp  5703  fncnv  6559  erinxp  8725  fpwwe2lem7  10550  fpwwe2lem8  10551  fpwwe2lem11  10554  nqerf  10843  nqerid  10846  isstruct  17082  pwsle  17415  psss  18505  psssdm2  18506  pi1cpbl  24961  pi1grplem  24966  br1cnvinxp  38250  brres2  38262  inxpss  38304  inxpss3  38307  idinxpssinxp2  38311  inxp2  38354  inxpxrn  38386