MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelres Structured version   Visualization version   GIF version

Theorem opelres 5308
Description: Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.)
Hypothesis
Ref Expression
opelres.1 𝐵 ∈ V
Assertion
Ref Expression
opelres (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴𝐷))

Proof of Theorem opelres
StepHypRef Expression
1 df-res 5039 . . 3 (𝐶𝐷) = (𝐶 ∩ (𝐷 × V))
21eleq2i 2679 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶 ∩ (𝐷 × V)))
3 elin 3757 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∩ (𝐷 × V)) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝐷 × V)))
4 opelres.1 . . . 4 𝐵 ∈ V
5 opelxp 5059 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (𝐷 × V) ↔ (𝐴𝐷𝐵 ∈ V))
64, 5mpbiran2 955 . . 3 (⟨𝐴, 𝐵⟩ ∈ (𝐷 × V) ↔ 𝐴𝐷)
76anbi2i 725 . 2 ((⟨𝐴, 𝐵⟩ ∈ 𝐶 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝐷 × V)) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴𝐷))
82, 3, 73bitri 284 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wcel 1976  Vcvv 3172  cin 3538  cop 4130   × cxp 5025  cres 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-opab 4638  df-xp 5033  df-res 5039
This theorem is referenced by:  brres  5309  opelresg  5310  opres  5312  dmres  5325  elres  5341  relssres  5343  iss  5353  restidsing  5363  restidsingOLD  5364  asymref  5417  ssrnres  5476  cnvresima  5526  ressn  5573  funssres  5829  fcnvres  5979  fvn0ssdmfun  6242  resiexg  6971  relexpindlem  13599  dprd2dlem1  18211  dprd2da  18212  hausdiag  21205  hauseqlcld  21206  ovoliunlem1  23021  h2hlm  27014  undmrnresiss  36712
  Copyright terms: Public domain W3C validator