Theorem brres 5977

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ⟨cop 4590   class class class wbr 5103   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  brresi  5979  dfima2  6058  predres  6342  elecres  8766  ttrclselem2  9727  axhcompl-zf  31600  fv1stcnv  36541  fv2ndcnv  36542  bj-idreseq  38084  bj-idreseqb  38085  brcnvepres  39205  brres2  39206  eldmres  39210  elrnres  39211  brinxprnres  39230  exanres  39234  eqres  39273  alrmomorn  39291  alrmomodm  39292  brxrn  39316  rnxrnres  39355  1cossres  39452  brressn  39464  eldm1cossres  39483  brssrres  39517  disjres  39777  antisymrelres  39799  dfdfat2  48198