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

Theorem op1stg 7687
Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
Assertion
Ref Expression
op1stg ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Proof of Theorem op1stg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4766 . . . 4 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveq2d 6653 . . 3 (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
42, 3eqeq12d 2817 . 2 (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5 opeq2 4768 . . 3 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
65fveqeq2d 6657 . 2 (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7 vex 3447 . . 3 𝑥 ∈ V
8 vex 3447 . . 3 𝑦 ∈ V
97, 8op1st 7683 . 2 (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
104, 6, 9vtocl2g 3523 1 ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  cop 4534  cfv 6328  1st c1st 7673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6287  df-fun 6330  df-fv 6336  df-1st 7675
This theorem is referenced by:  ot1stg  7689  ot2ndg  7690  br1steqg  7697  1stconst  7782  mposn  7785  curry2  7789  mpoxopn0yelv  7866  mpoxopoveq  7872  xpmapenlem  8672  1stinl  9344  1stinr  9346  fpwwe  10061  addpipq  10352  mulpipq  10355  ordpipq  10357  swrdval  14000  ruclem1  15579  qnumdenbi  16077  setsstruct  16518  oppccofval  16981  funcf2  17133  cofuval2  17152  resfval2  17158  resf1st  17159  isnat  17212  fucco  17227  homadm  17295  setcco  17338  estrcco  17375  xpcco  17428  xpchom2  17431  xpcco2  17432  evlf2  17463  curfval  17468  curf1cl  17473  uncf1  17481  uncf2  17482  diag11  17488  diag12  17489  diag2  17490  hof2fval  17500  yonedalem21  17518  yonedalem22  17523  mvmulfval  21150  imasdsf1olem  22983  ovolicc1  24123  ioombl1lem3  24167  ioombl1lem4  24168  addsqnreup  26030  brcgr  26697  opvtxfv  26800  fgreu  30438  fsuppcurry2  30491  sategoelfvb  32774  prv1n  32786  fvtransport  33601  bj-inftyexpiinv  34618  bj-finsumval0  34695  poimirlem17  35067  poimirlem24  35074  poimirlem27  35077  rngoablo2  35340  dvhopvadd  38382  dvhopvsca  38391  dvhopaddN  38403  dvhopspN  38404  etransclem44  42907  ovnsubaddlem1  43196  ovnlecvr2  43236  ovolval5lem2  43279  rngccoALTV  44599  ringccoALTV  44662
  Copyright terms: Public domain W3C validator