Theorem op1stg 7886

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 4813	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6813	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2753	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4814	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6817	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3445	. . 3 ⊢ 𝑥 ∈ V
8		vex 3445	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7882	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3519	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ⟨cop 4575  ‘cfv 6463  1^st c1st 7872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pr 5365  ax-un 7626

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-iota 6415  df-fun 6465  df-fv 6471  df-1st 7874

This theorem is referenced by:  ot1stg  7888  ot2ndg  7889  br1steqg  7896  1stconst  7983  mposn  7986  curry2  7990  opco1  8006  mpoxopn0yelv  8074  mpoxopoveq  8080  xpmapenlem  8984  1stinl  9753  1stinr  9755  fpwwe  10472  addpipq  10763  mulpipq  10766  ordpipq  10768  swrdval  14425  ruclem1  16009  qnumdenbi  16515  setsstruct  16944  oppccofval  17493  funcf2  17650  cofuval2  17669  resfval2  17675  resf1st  17676  isnat  17730  fucco  17747  homadm  17822  setcco  17865  estrcco  17913  xpcco  17967  xpchom2  17970  xpcco2  17971  evlf2  18003  curfval  18008  curf1cl  18013  uncf1  18021  uncf2  18022  diag11  18028  diag12  18029  diag2  18030  hof2fval  18040  yonedalem21  18058  yonedalem22  18063  mvmulfval  21762  imasdsf1olem  23597  ovolicc1  24751  ioombl1lem3  24795  ioombl1lem4  24796  addsqnreup  26662  brcgr  27376  opvtxfv  27482  fgreu  31117  fsuppcurry2  31169  sategoelfvb  33487  prv1n  33499  addsval  34187  fvtransport  34395  bj-inftyexpiinv  35439  bj-finsumval0  35516  poimirlem17  35854  poimirlem24  35861  poimirlem27  35864  rngoablo2  36127  dvhopvadd  39319  dvhopvsca  39328  dvhopaddN  39340  dvhopspN  39341  etransclem44  44063  ovnsubaddlem1  44353  ovnlecvr2  44393  ovolval5lem2  44436  rngccoALTV  45805  ringccoALTV  45868