Theorem op1stg 7997

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 6878	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2776	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4834	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6882	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3454	. . 3 ⊢ 𝑥 ∈ V
8		vex 3454	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7993	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3533	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4590  ‘cfv 6528  1^st c1st 7983

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-iota 6484  df-fun 6530  df-fv 6536  df-1st 7985

This theorem is used by:  ot1stg  7999  ot2ndg  8000  br1steqg  8007  1stconst  8095  mposn  8098  curry2  8102  opco1  8118  mpoxopn0yelv  8209  mpoxopoveq  8215  xpmapenlem  9142  1stinl  9965  1stinr  9967  fpwwe  10688  addpipq  10979  mulpipq  10982  ordpipq  10984  swrdval  14744  ruclem1  16352  qnumdenbi  16868  setsstruct  17301  oppccofval  17837  funcf2  17990  cofuval2  18009  resfval2  18015  resf1st  18016  isnat  18072  fucco  18087  homadm  18162  setcco  18205  estrcco  18251  xpcco  18304  xpchom2  18307  xpcco2  18308  evlf2  18339  curfval  18344  curf1cl  18349  uncf1  18357  uncf2  18358  diag11  18364  diag12  18365  diag2  18366  hof2fval  18376  yonedalem21  18394  yonedalem22  18399  mvmulfval  22804  imasdsf1olem  24639  ovolicc1  25784  ioombl1lem3  25828  ioombl1lem4  25829  addsqnreup  27719  addsval  28267  mulsval  28414  brcgr  29397  opvtxfv  29501  fgreu  33184  fsuppcurry2  33236  erlbrd  33743  erld2  33746  rlocaddval  33749  rlocmulval  33750  fracerl  33787  sategoelfvb  36099  prv1n  36111  fvtransport  36713  bj-inftyexpiinv  38043  bj-finsumval0  38120  poimirlem17  38469  poimirlem24  38476  poimirlem27  38479  rngoablo2  38757  dvhopvadd  42064  dvhopvsca  42073  dvhopaddN  42085  dvhopspN  42086  etransclem44  47204  ovnsubaddlem1  47496  ovnlecvr2  47536  ovolval5lem2  47579  gpgedgiov  49079  gpgedg2ov  49080  gpgedg2iv  49081  rngccoALTV  49284  ringccoALTV  49318  func1st  50101  oppf1st2nd  50155  upfval3  50202  swapf1val  50291  fucofval  50343  fuco111  50354  fuco21  50360  fucoid  50372  precofval3  50395  prcofvala  50401  prcofval  50402  lanfval  50637  ranfval  50638