Theorem brres 5860

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5066   ↾ cres 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-res 5567

This theorem is referenced by:  brresi  5862  dfima2  5931  axhcompl-zf  28775  fv1stcnv  33020  fv2ndcnv  33021  bj-idreseq  34457  bj-idreseqb  34458  brcnvepres  35543  brres2  35544  eldmres  35545  elecres  35549  brinxprnres  35563  exanres  35567  eqres  35612  alrmomorn  35627  alrmomodm  35628  brxrn  35641  rnxrnres  35662  1cossres  35689  eldm1cossres  35715  brssrres  35759  dfdfat2  43347