Theorem brresi 5978

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  dfres2  6032  poirr2  6117  cores  6250  resco  6251  rnco  6253  rncoOLD  6254  dfpo2  6299  fnres  6666  fvres  6904  nfunsn  6924  eqfunresadj  7370  1stconst  8111  2ndconst  8112  fsplit  8128  fprlem1  8318  ttrclresv  9718  ttrclselem2  9727  frrlem15  9761  setrec2lem2  9976  dprd2da  20258  metustid  24873  dvres  26231  dvres2  26232  ltgov  29060  hlimadd  31795  hhcmpl  31802  hhcms  31805  hlim0  31837  dfdm5  36537  dfrn5  36538  txpss3v  36640  brtxp  36642  pprodss4v  36646  brpprod  36647  brimg  36699  brapply  36700  funpartfun  36707  dfrdg4  36715  xrnss3v  39314  funressnfv  48113  funressnvmo  48115  afv2res  48309  tposres0  49985