Theorem brresi 5985

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3453   class class class wbr 5107   ↾ cres 5661

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-res 5671

This theorem is used by:  dfres2  6041  poirr2  6122  cores  6249  resco  6250  rnco  6252  rncoOLD  6253  dfpo2  6298  fnres  6663  fvres  6901  nfunsn  6921  eqfunresadj  7366  1stconst  8100  2ndconst  8101  fsplit  8117  fprlem1  8302  ttrclresv  9699  ttrclselem2  9708  frrlem15  9742  dprd2da  20172  metustid  24781  dvres  26140  dvres2  26141  ltgov  28937  hlimadd  31660  hhcmpl  31667  hhcms  31670  hlim0  31702  dfdm5  36339  dfrn5  36340  txpss3v  36442  brtxp  36444  pprodss4v  36448  brpprod  36449  brimg  36501  brapply  36502  funpartfun  36509  dfrdg4  36517  xrnss3v  39116  funressnfv  47918  funressnvmo  47920  afv2res  48114  tposres0  49790  setrec2lem2  50607