Theorem brres 5201

Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)

Hypothesis

Ref	Expression
opelres.1	|- B e. _V

Assertion

Ref	Expression
brres	|- ( A ( C |` D ) B <-> ( A C B /\ A e. D ) )

Proof of Theorem brres

Step	Hyp	Ref	Expression
1		opelres.1	. . 3 |- B e. _V
2	1	opelres 5200	. 2 |- ( <. A , B >. e. ( C |` D ) <-> ( <. A , B >. e. C /\ A e. D ) )
3		df-br 4377	. 2 |- ( A ( C |` D ) B <-> <. A , B >. e. ( C |` D ) )
4		df-br 4377	. . 3 |- ( A C B <-> <. A , B >. e. C )
5	4	anbi1i 695	. 2 |- ( ( A C B /\ A e. D ) <-> ( <. A , B >. e. C /\ A e. D ) )
6	2, 3, 5	3bitr4i 277	1 |- ( A ( C |` D ) B <-> ( A C B /\ A e. D ) )

Syntax hints:   <-> wb 184   /\ wa 369   e. wcel 1757   _Vcvv 3054   <.cop 3967   class class class wbr 4376   |` cres 4926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-xp 4930  df-res 4936

This theorem is referenced by:  dfres2  5242  dfima2  5255  poirr2  5306  cores  5425  resco  5426  rnco  5428  fnres  5611  fvres  5789  nfunsn  5806  1stconst  6747  2ndconst  6748  fsplit  6763  dprd2da  16632  metustidOLD  20236  metustid  20237  dvres  21488  dvres2  21489  axhcompl-zf  24521  hlimadd  24716  hhcmpl  24723  hhcms  24726  hlim0  24759  dfpo2  27685  dfdm5  27707  dfrn5  27708  wfrlem5  27848  frrlem5  27892  txpss3v  28029  brtxp  28031  pprodss4v  28035  brpprod  28036  brimg  28088  brapply  28089  funpartfun  28094  dfrdg4  28101  funressnfv  30158  dfdfat2  30161