Theorem brresi 5942

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3427   class class class wbr 5074   ↾ cres 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-res 5632

This theorem is referenced by:  dfres2  5995  poirr2  6076  cores  6202  resco  6203  rnco  6205  rncoOLD  6206  dfpo2  6249  fnres  6614  fvres  6848  nfunsn  6868  eqfunresadj  7304  1stconst  8039  2ndconst  8040  fsplit  8056  fprlem1  8239  ttrclresv  9627  ttrclselem2  9636  frrlem15  9670  dprd2da  20008  metustid  24507  dvres  25866  dvres2  25867  ltgov  28653  hlimadd  31252  hhcmpl  31259  hhcms  31262  hlim0  31294  dfdm5  35943  dfrn5  35944  txpss3v  36046  brtxp  36048  pprodss4v  36052  brpprod  36053  brimg  36105  brapply  36106  funpartfun  36113  dfrdg4  36121  xrnss3v  38690  funressnfv  47479  funressnvmo  47481  afv2res  47675  tposres0  49340  setrec2lem2  50157