Theorem brresi 5976

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2144  Vcvv 3456   class class class wbr 5102   ↾ cres 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-res 5661

This theorem is referenced by:  dfres2  6032  poirr2  6113  cores  6238  resco  6239  rnco  6241  rncoOLD  6242  dfpo2  6285  fnres  6650  fvres  6888  nfunsn  6908  eqfunresadj  7346  1stconst  8081  2ndconst  8082  fsplit  8098  fprlem1  8283  ttrclresv  9674  ttrclselem2  9683  frrlem15  9717  dprd2da  20086  metustid  24616  dvres  25975  dvres2  25976  ltgov  28768  hlimadd  31398  hhcmpl  31405  hhcms  31408  hlim0  31440  dfdm5  36128  dfrn5  36129  txpss3v  36231  brtxp  36233  pprodss4v  36237  brpprod  36238  brimg  36290  brapply  36291  funpartfun  36298  dfrdg4  36306  xrnss3v  38885  funressnfv  47642  funressnvmo  47644  afv2res  47838  tposres0  49503  setrec2lem2  50320