Theorem brresi 5897

Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)

Hypothesis

Ref	Expression
opelresi.1	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
brresi	⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))

Proof of Theorem brresi

Step	Hyp	Ref	Expression
1		opelresi.1	. 2 ⊢ 𝐶 ∈ V
2		brres 5895	. 2 ⊢ (𝐶 ∈ V → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2109  Vcvv 3430   class class class wbr 5078   ↾ cres 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-xp 5594  df-res 5600

This theorem is referenced by:  dfres2  5946  poirr2  6026  cores  6150  resco  6151  rnco  6153  dfpo2  6196  fnres  6555  fvres  6787  nfunsn  6805  1stconst  7924  2ndconst  7925  fsplit  7941  fsplitOLD  7942  fprlem1  8100  wfrlem5OLD  8128  ttrclresv  9436  ttrclselem2  9445  frrlem15  9499  dprd2da  19626  metustid  23691  dvres  25056  dvres2  25057  ltgov  26939  hlimadd  29534  hhcmpl  29541  hhcms  29544  hlim0  29576  eqfunresadj  33714  dfdm5  33726  dfrn5  33727  txpss3v  34159  brtxp  34161  pprodss4v  34165  brpprod  34166  brimg  34218  brapply  34219  funpartfun  34224  dfrdg4  34232  xrnss3v  36481  funressnfv  44488  funressnvmo  44490  afv2res  44682  setrec2lem2  46352