Theorem brres 5268

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 5267	. 2 |- ( <. A , B >. e. ( C |` D ) <-> ( <. A , B >. e. C /\ A e. D ) )
3		df-br 4440	. 2 |- ( A ( C |` D ) B <-> <. A , B >. e. ( C |` D ) )
4		df-br 4440	. . 3 |- ( A C B <-> <. A , B >. e. C )
5	4	anbi1i 693	. 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 367   e. wcel 1823   _Vcvv 3106   <.cop 4022   class class class wbr 4439   |` cres 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-res 5000

This theorem is referenced by:  dfres2  5314  dfima2  5327  poirr2  5379  cores  5493  resco  5494  rnco  5496  fnres  5679  fvres  5862  nfunsn  5879  1stconst  6861  2ndconst  6862  fsplit  6878  dprd2da  17289  metustidOLD  21231  metustid  21232  dvres  22484  dvres2  22485  ltgov  24187  axhcompl-zf  26116  hlimadd  26311  hhcmpl  26318  hhcms  26321  hlim0  26354  dfpo2  29428  dfdm5  29449  dfrn5  29450  wfrlem5  29590  frrlem5  29634  txpss3v  29759  brtxp  29761  pprodss4v  29765  brpprod  29766  brimg  29818  brapply  29819  funpartfun  29824  dfrdg4  29831  funressnfv  32455  dfdfat2  32458