Theorem brres 5972

Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.)

Assertion

Ref	Expression
brres	⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))

Proof of Theorem brres

Step	Hyp	Ref	Expression
1		opelres 5971	. 2 ⊢ (𝐶 ∈ 𝑉 → (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
2		df-br 5101	. 2 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴))
3		df-br 5101	. . 3 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
4	3	anbi2i 632	. 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
5	1, 2, 4	3bitr4g 316	1 ⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  ⟨cop 4588   class class class wbr 5100   ↾ cres 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-res 5659

This theorem is referenced by:  brresi  5974  dfima2  6051  predres  6326  elecres  8727  ttrclselem2  9681  axhcompl-zf  31198  fv1stcnv  36124  fv2ndcnv  36125  bj-idreseq  37651  bj-idreseqb  37652  brcnvepres  38768  brres2  38769  eldmres  38773  elrnres  38774  brinxprnres  38793  exanres  38797  eqres  38836  alrmomorn  38854  alrmomodm  38855  brxrn  38879  rnxrnres  38918  1cossres  39015  brressn  39027  eldm1cossres  39046  brssrres  39080  disjres  39340  antisymrelres  39362  dfdfat2  47719