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 205   ∧ wa 397   ∈ wcel 2107  Vcvv 3475   class class class wbr 5147   ↾ cres 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-res 5687

This theorem is referenced by:  dfres2  6039  poirr2  6122  cores  6245  resco  6246  rnco  6248  dfpo2  6292  fnres  6674  fvres  6907  nfunsn  6930  eqfunresadj  7352  1stconst  8081  2ndconst  8082  fsplit  8098  fprlem1  8280  wfrlem5OLD  8308  ttrclresv  9708  ttrclselem2  9717  frrlem15  9748  dprd2da  19904  metustid  24045  dvres  25410  dvres2  25411  ltgov  27828  hlimadd  30424  hhcmpl  30431  hhcms  30434  hlim0  30466  dfdm5  34682  dfrn5  34683  txpss3v  34788  brtxp  34790  pprodss4v  34794  brpprod  34795  brimg  34847  brapply  34848  funpartfun  34853  dfrdg4  34861  xrnss3v  37180  funressnfv  45688  funressnvmo  45690  afv2res  45882  setrec2lem2  47641