Theorem brres 6016

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 6015	. 2 ⊢ (𝐶 ∈ 𝑉 → (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
2		df-br 5167	. 2 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴))
3		df-br 5167	. . 3 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
4	3	anbi2i 622	. 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
5	1, 2, 4	3bitr4g 314	1 ⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ⟨cop 4654   class class class wbr 5166   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-res 5712

This theorem is referenced by:  brresi  6018  dfima2  6091  predres  6371  ttrclselem2  9795  axhcompl-zf  31030  fv1stcnv  35740  fv2ndcnv  35741  bj-idreseq  37128  bj-idreseqb  37129  brcnvepres  38223  brres2  38224  eldmres  38226  elrnres  38227  elecres  38233  brinxprnres  38247  exanres  38251  eqres  38296  alrmomorn  38314  alrmomodm  38315  brxrn  38330  rnxrnres  38355  1cossres  38385  brressn  38397  eldm1cossres  38416  brssrres  38460  disjres  38700  antisymrelres  38719  dfdfat2  47043