Theorem brresi 5989

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-res 5667

This theorem is used by:  dfres2  6044  poirr2  6129  cores  6262  resco  6263  rnco  6265  rncoOLD  6266  idresdmsscocnv1  6274  dfpo2  6314  fnres  6685  fvres  6924  nfunsn  6944  eqfunresadj  7390  1stconst  8135  2ndconst  8136  fsplit  8152  fprlem1  8343  ttrclresv  9742  ttrclselem2  9751  frrlem15  9785  setrec2lem2  10000  dprd2da  20285  metustid  24900  dvres  26258  dvres2  26259  ltgov  29087  hlimadd  31822  hhcmpl  31829  hhcms  31832  hlim0  31864  dfdm5  36714  dfrn5  36715  txpss3v  36817  brtxp  36819  pprodss4v  36823  brpprod  36824  brimg  36876  brapply  36877  funpartfun  36884  dfrdg4  36892  xrnss3v  39504  funressnfv  48316  funressnvmo  48318  afv2res  48512  tposres0  50193