Theorem op1stg 7984

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.

Step	Hyp	Ref	Expression
1		opeq1 4833	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6873	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2780	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4834	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6877	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3460	. . 3 ⊢ 𝑥 ∈ V
8		vex 3460	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7980	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3540	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ⟨cop 4590  ‘cfv 6523  1^st c1st 7970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-iota 6479  df-fun 6525  df-fv 6531  df-1st 7972

This theorem is referenced by:  ot1stg  7986  ot2ndg  7987  br1steqg  7994  1stconst  8081  mposn  8084  curry2  8088  opco1  8104  mpoxopn0yelv  8195  mpoxopoveq  8201  xpmapenlem  9118  1stinl  9887  1stinr  9889  fpwwe  10606  addpipq  10897  mulpipq  10900  ordpipq  10902  swrdval  14659  ruclem1  16265  qnumdenbi  16781  setsstruct  17214  oppccofval  17750  funcf2  17903  cofuval2  17922  resfval2  17928  resf1st  17929  isnat  17985  fucco  18000  homadm  18075  setcco  18118  estrcco  18164  xpcco  18217  xpchom2  18220  xpcco2  18221  evlf2  18252  curfval  18257  curf1cl  18262  uncf1  18270  uncf2  18271  diag11  18277  diag12  18278  diag2  18279  hof2fval  18289  yonedalem21  18307  yonedalem22  18312  mvmulfval  22604  imasdsf1olem  24435  ovolicc1  25580  ioombl1lem3  25624  ioombl1lem4  25625  addsqnreup  27509  addsval  28057  mulsval  28204  brcgr  29103  opvtxfv  29207  fgreu  32875  fsuppcurry2  32929  erlbrd  33446  erld2  33449  rlocaddval  33452  rlocmulval  33453  fracerl  33495  sategoelfvb  35774  prv1n  35786  fvtransport  36387  bj-inftyexpiinv  37705  bj-finsumval0  37782  poimirlem17  38141  poimirlem24  38148  poimirlem27  38151  rngoablo2  38413  dvhopvadd  41722  dvhopvsca  41731  dvhopaddN  41743  dvhopspN  41744  etransclem44  46857  ovnsubaddlem1  47149  ovnlecvr2  47189  ovolval5lem2  47232  gpgedgiov  48692  gpgedg2ov  48693  gpgedg2iv  48694  rngccoALTV  48898  ringccoALTV  48932  func1st  49703  oppf1st2nd  49757  upfval3  49804  swapf1val  49893  fucofval  49945  fuco111  49956  fuco21  49962  fucoid  49974  precofval3  49997  prcofvala  50003  prcofval  50004  lanfval  50239  ranfval  50240