MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brres Structured version   Visualization version   GIF version

Theorem brres 5310
Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.)
Hypothesis
Ref Expression
opelres.1 𝐵 ∈ V
Assertion
Ref Expression
brres (𝐴(𝐶𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐴𝐷))

Proof of Theorem brres
StepHypRef Expression
1 opelres.1 . . 3 𝐵 ∈ V
21opelres 5309 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴𝐷))
3 df-br 4579 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷))
4 df-br 4579 . . 3 (𝐴𝐶𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝐶)
54anbi1i 727 . 2 ((𝐴𝐶𝐵𝐴𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴𝐷))
62, 3, 53bitr4i 291 1 (𝐴(𝐶𝐷)𝐵 ↔ (𝐴𝐶𝐵𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wcel 1977  Vcvv 3173  cop 4131   class class class wbr 4578  cres 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579  df-opab 4639  df-xp 5034  df-res 5040
This theorem is referenced by:  dfres2  5359  dfima2  5374  poirr2  5426  cores  5541  resco  5542  rnco  5544  fnres  5907  fvres  6102  nfunsn  6120  1stconst  7130  2ndconst  7131  fsplit  7147  wfrlem5  7284  dprd2da  18213  metustid  22117  dvres  23426  dvres2  23427  ltgov  25238  axhcompl-zf  27033  hlimadd  27228  hhcmpl  27235  hhcms  27238  hlim0  27270  dfpo2  30692  dfdm5  30715  dfrn5  30716  frrlem5  30822  txpss3v  30949  brtxp  30951  pprodss4v  30955  brpprod  30956  brimg  31008  brapply  31009  funpartfun  31014  dfrdg4  31022  funressnfv  39651  dfdfat2  39655
  Copyright terms: Public domain W3C validator