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

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

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