Theorem brresi 5962

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110   ↾ cres 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653

This theorem is referenced by:  dfres2  6015  poirr2  6100  cores  6225  resco  6226  rnco  6228  dfpo2  6272  fnres  6648  fvres  6880  nfunsn  6903  eqfunresadj  7338  1stconst  8082  2ndconst  8083  fsplit  8099  fprlem1  8282  ttrclresv  9677  ttrclselem2  9686  frrlem15  9717  dprd2da  19981  metustid  24449  dvres  25819  dvres2  25820  ltgov  28531  hlimadd  31129  hhcmpl  31136  hhcms  31139  hlim0  31171  dfdm5  35767  dfrn5  35768  txpss3v  35873  brtxp  35875  pprodss4v  35879  brpprod  35880  brimg  35932  brapply  35933  funpartfun  35938  dfrdg4  35946  xrnss3v  38361  funressnfv  47048  funressnvmo  47050  afv2res  47244  tposres0  48869  setrec2lem2  49687