Theorem brresi 6009

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 6007	. 2 ⊢ (𝐶 ∈ V → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
3	1, 2	ax-mp 5	1 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2106  Vcvv 3478   class class class wbr 5148   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-res 5701

This theorem is referenced by:  dfres2  6061  poirr2  6147  cores  6271  resco  6272  rnco  6274  dfpo2  6318  fnres  6696  fvres  6926  nfunsn  6949  eqfunresadj  7380  1stconst  8124  2ndconst  8125  fsplit  8141  fprlem1  8324  wfrlem5OLD  8352  ttrclresv  9755  ttrclselem2  9764  frrlem15  9795  dprd2da  20077  metustid  24583  dvres  25961  dvres2  25962  ltgov  28620  hlimadd  31222  hhcmpl  31229  hhcms  31232  hlim0  31264  dfdm5  35754  dfrn5  35755  txpss3v  35860  brtxp  35862  pprodss4v  35866  brpprod  35867  brimg  35919  brapply  35920  funpartfun  35925  dfrdg4  35933  xrnss3v  38354  funressnfv  46993  funressnvmo  46995  afv2res  47189  setrec2lem2  48925