Theorem brresi 5975

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Vcvv 3459   class class class wbr 5119   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-res 5666

This theorem is referenced by:  dfres2  6028  poirr2  6113  cores  6238  resco  6239  rnco  6241  dfpo2  6285  fnres  6665  fvres  6895  nfunsn  6918  eqfunresadj  7353  1stconst  8099  2ndconst  8100  fsplit  8116  fprlem1  8299  wfrlem5OLD  8327  ttrclresv  9731  ttrclselem2  9740  frrlem15  9771  dprd2da  20025  metustid  24493  dvres  25864  dvres2  25865  ltgov  28576  hlimadd  31174  hhcmpl  31181  hhcms  31184  hlim0  31216  dfdm5  35790  dfrn5  35791  txpss3v  35896  brtxp  35898  pprodss4v  35902  brpprod  35903  brimg  35955  brapply  35956  funpartfun  35961  dfrdg4  35969  xrnss3v  38390  funressnfv  47072  funressnvmo  47074  afv2res  47268  tposres0  48852  setrec2lem2  49558