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

Theorem op1stg 7222
 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 4433 . . . 4 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
21fveq2d 6233 . . 3 (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
42, 3eqeq12d 2666 . 2 (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5 opeq2 4434 . . . 4 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
65fveq2d 6233 . . 3 (𝑦 = 𝐵 → (1st ‘⟨𝐴, 𝑦⟩) = (1st ‘⟨𝐴, 𝐵⟩))
76eqeq1d 2653 . 2 (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
8 vex 3234 . . 3 𝑥 ∈ V
9 vex 3234 . . 3 𝑦 ∈ V
108, 9op1st 7218 . 2 (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
114, 7, 10vtocl2g 3301 1 ((𝐴𝑉𝐵𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ⟨cop 4216  ‘cfv 5926  1st c1st 7208 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fv 5934  df-1st 7210 This theorem is referenced by:  ot1stg  7224  ot2ndg  7225  br1steqg  7232  1stconst  7310  mpt2sn  7313  curry2  7317  mpt2xopn0yelv  7384  mpt2xopoveq  7390  xpmapenlem  8168  fpwwe  9506  addpipq  9797  mulpipq  9800  ordpipq  9802  swrdval  13462  ruclem1  15004  qnumdenbi  15499  setsstruct  15945  oppccofval  16423  funcf2  16575  cofuval2  16594  resfval2  16600  resf1st  16601  isnat  16654  fucco  16669  homadm  16737  setcco  16780  estrcco  16817  xpcco  16870  xpchom2  16873  xpcco2  16874  evlf2  16905  curfval  16910  curf1cl  16915  uncf1  16923  uncf2  16924  diag11  16930  diag12  16931  diag2  16932  hof2fval  16942  yonedalem21  16960  yonedalem22  16965  mvmulfval  20396  imasdsf1olem  22225  ovolicc1  23330  ioombl1lem3  23374  ioombl1lem4  23375  brcgr  25825  opvtxfv  25929  fgreu  29599  fvtransport  32264  bj-elid3  33217  bj-inftyexpiinv  33225  bj-finsumval0  33277  poimirlem17  33556  poimirlem24  33563  poimirlem27  33566  rngoablo2  33838  dvhopvadd  36699  dvhopvsca  36708  dvhopaddN  36720  dvhopspN  36721  etransclem44  40813  ovnsubaddlem1  41105  ovnlecvr2  41145  ovolval5lem2  41188  rngccoALTV  42313  ringccoALTV  42376
 Copyright terms: Public domain W3C validator