Theorem brresi 5939

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092   ↾ cres 5621

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 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-res 5631

This theorem is referenced by:  dfres2  5992  poirr2  6073  cores  6198  resco  6199  rnco  6201  dfpo2  6244  fnres  6609  fvres  6841  nfunsn  6862  eqfunresadj  7297  1stconst  8033  2ndconst  8034  fsplit  8050  fprlem1  8233  ttrclresv  9613  ttrclselem2  9622  frrlem15  9653  dprd2da  19923  metustid  24440  dvres  25810  dvres2  25811  ltgov  28542  hlimadd  31137  hhcmpl  31144  hhcms  31147  hlim0  31179  dfdm5  35756  dfrn5  35757  txpss3v  35862  brtxp  35864  pprodss4v  35868  brpprod  35869  brimg  35921  brapply  35922  funpartfun  35927  dfrdg4  35935  xrnss3v  38350  funressnfv  47037  funressnvmo  47039  afv2res  47233  tposres0  48871  setrec2lem2  49689