Theorem brresi 5945

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Vcvv 3438   class class class wbr 5096   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634

This theorem is referenced by:  dfres2  5998  poirr2  6079  cores  6205  resco  6206  rnco  6208  rncoOLD  6209  dfpo2  6252  fnres  6617  fvres  6851  nfunsn  6871  eqfunresadj  7304  1stconst  8040  2ndconst  8041  fsplit  8057  fprlem1  8240  ttrclresv  9624  ttrclselem2  9633  frrlem15  9667  dprd2da  19971  metustid  24496  dvres  25866  dvres2  25867  ltgov  28618  hlimadd  31217  hhcmpl  31224  hhcms  31227  hlim0  31259  dfdm5  35916  dfrn5  35917  txpss3v  36019  brtxp  36021  pprodss4v  36025  brpprod  36026  brimg  36078  brapply  36079  funpartfun  36086  dfrdg4  36094  xrnss3v  38505  funressnfv  47231  funressnvmo  47233  afv2res  47427  tposres0  49064  setrec2lem2  49881