Theorem opelresi 5990

Description: Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)

Hypothesis

Ref	Expression
opelresi.1	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
opelresi	⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))

Proof of Theorem opelresi

Step	Hyp	Ref	Expression
1		opelresi.1	. 2 ⊢ 𝐶 ∈ V
2		opelres 5988	. 2 ⊢ (𝐶 ∈ V → (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
3	1, 2	ax-mp 5	1 ⊢ (⟨𝐵, 𝐶⟩ ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2150  Vcvv 3462  ⟨cop 4600   ↾ cres 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-sep 5262  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5179  df-xp 5671  df-res 5677

This theorem is referenced by:  opres  5992  dmres  6015  relssres  6025  iss  6041  restidsing  6059  asymref  6120  ssrnres  6180  cnvresima  6235  ressn  6290  funssres  6584  fcnvres  6759  fvn0ssdmfun  7073  relexpindlem  15103  dprd2dlem1  20116  dprd2da  20117  hausdiag  23785  hauseqlcld  23786  ovoliunlem1  25644  undmrnresiss  44282