Theorem brresi 5860

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2110  Vcvv 3408   class class class wbr 5053   ↾ cres 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-xp 5557  df-res 5563

This theorem is referenced by:  dfres2  5909  poirr2  5989  cores  6113  resco  6114  rnco  6116  fnres  6504  fvres  6736  nfunsn  6754  1stconst  7868  2ndconst  7869  fsplit  7885  fsplitOLD  7886  fprlem1  8041  wfrlem5  8059  frrlem15  9373  dprd2da  19429  metustid  23452  dvres  24808  dvres2  24809  ltgov  26688  hlimadd  29274  hhcmpl  29281  hhcms  29284  hlim0  29316  dfpo2  33441  eqfunresadj  33454  dfdm5  33466  dfrn5  33467  ttrclresv  33516  txpss3v  33917  brtxp  33919  pprodss4v  33923  brpprod  33924  brimg  33976  brapply  33977  funpartfun  33982  dfrdg4  33990  xrnss3v  36239  funressnfv  44209  funressnvmo  44211  afv2res  44403  setrec2lem2  46071