Theorem brresi 6006

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143   ↾ cres 5687

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  dfres2  6059  poirr2  6144  cores  6269  resco  6270  rnco  6272  dfpo2  6316  fnres  6695  fvres  6925  nfunsn  6948  eqfunresadj  7380  1stconst  8125  2ndconst  8126  fsplit  8142  fprlem1  8325  wfrlem5OLD  8353  ttrclresv  9757  ttrclselem2  9766  frrlem15  9797  dprd2da  20062  metustid  24567  dvres  25946  dvres2  25947  ltgov  28605  hlimadd  31212  hhcmpl  31219  hhcms  31222  hlim0  31254  dfdm5  35773  dfrn5  35774  txpss3v  35879  brtxp  35881  pprodss4v  35885  brpprod  35886  brimg  35938  brapply  35939  funpartfun  35944  dfrdg4  35952  xrnss3v  38373  funressnfv  47055  funressnvmo  47057  afv2res  47251  tposres0  48777  setrec2lem2  49213