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 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103   ↾ cres 5650

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 2732  ax-sep 5249  ax-pr 5391

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5654  df-res 5660

This theorem is used by:  dfres2  6032  poirr2  6113  cores  6240  resco  6241  rnco  6243  rncoOLD  6244  dfpo2  6289  fnres  6655  fvres  6893  nfunsn  6913  eqfunresadj  7359  1stconst  8095  2ndconst  8096  fsplit  8112  fprlem1  8297  ttrclresv  9696  ttrclselem2  9705  frrlem15  9739  setrec2lem2  9933  dprd2da  20205  metustid  24820  dvres  26178  dvres2  26179  ltgov  28979  hlimadd  31714  hhcmpl  31721  hhcms  31724  hlim0  31756  dfdm5  36453  dfrn5  36454  txpss3v  36556  brtxp  36558  pprodss4v  36562  brpprod  36563  brimg  36615  brapply  36616  funpartfun  36623  dfrdg4  36631  xrnss3v  39227  funressnfv  48029  funressnvmo  48031  afv2res  48225  tposres0  49901