Theorem brresi 5947

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∈ wcel 2121  Vcvv 3433   class class class wbr 5075   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-res 5633

This theorem is referenced by:  dfres2  6000  poirr2  6081  cores  6204  resco  6205  rnco  6207  rncoOLD  6208  dfpo2  6251  fnres  6616  fvres  6850  nfunsn  6870  eqfunresadj  7308  1stconst  8043  2ndconst  8044  fsplit  8060  fprlem1  8244  ttrclresv  9633  ttrclselem2  9642  frrlem15  9676  dprd2da  20014  metustid  24541  dvres  25900  dvres2  25901  ltgov  28687  hlimadd  31286  hhcmpl  31293  hhcms  31296  hlim0  31328  dfdm5  36016  dfrn5  36017  txpss3v  36119  brtxp  36121  pprodss4v  36125  brpprod  36126  brimg  36178  brapply  36179  funpartfun  36186  dfrdg4  36194  xrnss3v  38763  funressnfv  47520  funressnvmo  47522  afv2res  47716  tposres0  49381  setrec2lem2  50198