Theorem brresi 5988

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  Vcvv 3461   class class class wbr 5111   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-opab 5176  df-xp 5668  df-res 5674

This theorem is referenced by:  dfres2  6044  poirr2  6125  cores  6251  resco  6252  rnco  6254  rncoOLD  6255  dfpo2  6298  fnres  6663  fvres  6901  nfunsn  6921  eqfunresadj  7359  1stconst  8095  2ndconst  8096  fsplit  8112  fprlem1  8297  ttrclresv  9686  ttrclselem2  9695  frrlem15  9729  dprd2da  20114  metustid  24680  dvres  26039  dvres2  26040  ltgov  28832  hlimadd  31486  hhcmpl  31493  hhcms  31496  hlim0  31528  dfdm5  36198  dfrn5  36199  txpss3v  36301  brtxp  36303  pprodss4v  36307  brpprod  36308  brimg  36360  brapply  36361  funpartfun  36368  dfrdg4  36376  xrnss3v  38955  funressnfv  47704  funressnvmo  47706  afv2res  47900  tposres0  49575  setrec2lem2  50392