Theorem brxp 5304

Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.)

Assertion

Ref	Expression
brxp	⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Proof of Theorem brxp

Step	Hyp	Ref	Expression
1		df-br 4805	. 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
2		opelxp 5303	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
3	1, 2	bitri 264	1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 196   ∧ wa 383   ∈ wcel 2139  ⟨cop 4327   class class class wbr 4804   × cxp 5264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272

This theorem is referenced by:  brrelex12  5312  brel  5325  brinxp2  5337  eqbrrdva  5447  ssrelrn  5470  xpidtr  5676  xpco  5836  isocnv3  6746  tpostpos  7542  swoer  7943  erinxp  7990  ecopover  8020  infxpenlem  9046  fpwwe2lem6  9669  fpwwe2lem7  9670  fpwwe2lem9  9672  fpwwe2lem12  9675  fpwwe2lem13  9676  fpwwe2  9677  ltxrlt  10320  ltxr  12162  xpcogend  13934  xpsfrnel2  16447  invfuc  16855  elhoma  16903  efglem  18349  gsumdixp  18829  gsumbagdiag  19598  psrass1lem  19599  opsrtoslem2  19707  znleval  20125  gsumcom3fi  20428  brelg  29749  posrasymb  29987  trleile  29996  metider  30267  mclsppslem  31808  dfpo2  31973  slenlt  32204  dfon3  32326  brbigcup  32332  brsingle  32351  brimage  32360  brcart  32366  brapply  32372  brcup  32373  brcap  32374  funpartlem  32376  dfrdg4  32385  brub  32388  itg2gt0cn  33796  brinxp2ALTV  34376