Theorem op1stg 7515

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 4678	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6505	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2793	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4679	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6509	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3418	. . 3 ⊢ 𝑥 ∈ V
8		vex 3418	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7511	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3490	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ⟨cop 4448  ‘cfv 6190  1^st c1st 7501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-iota 6154  df-fun 6192  df-fv 6198  df-1st 7503

This theorem is referenced by:  ot1stg  7517  ot2ndg  7518  br1steqg  7525  1stconst  7605  mposn  7608  curry2  7612  mpoxopn0yelv  7684  mpoxopoveq  7690  xpmapenlem  8482  1stinl  9152  1stinr  9154  fpwwe  9868  addpipq  10159  mulpipq  10162  ordpipq  10164  swrdval  13809  ruclem1  15447  qnumdenbi  15943  setsstruct  16382  oppccofval  16847  funcf2  16999  cofuval2  17018  resfval2  17024  resf1st  17025  isnat  17078  fucco  17093  homadm  17161  setcco  17204  estrcco  17241  xpcco  17294  xpchom2  17297  xpcco2  17298  evlf2  17329  curfval  17334  curf1cl  17339  uncf1  17347  uncf2  17348  diag11  17354  diag12  17355  diag2  17356  hof2fval  17366  yonedalem21  17384  yonedalem22  17389  mvmulfval  20858  imasdsf1olem  22689  ovolicc1  23823  ioombl1lem3  23867  ioombl1lem4  23868  addsqnreup  25724  brcgr  26392  opvtxfv  26495  fgreu  30182  fsuppcurry2  30217  fvtransport  33014  bj-elid3  33940  bj-inftyexpiinv  33959  bj-finsumval0  34030  poimirlem17  34350  poimirlem24  34357  poimirlem27  34360  rngoablo2  34629  dvhopvadd  37674  dvhopvsca  37683  dvhopaddN  37695  dvhopspN  37696  etransclem44  41995  ovnsubaddlem1  42284  ovnlecvr2  42324  ovolval5lem2  42367  rngccoALTV  43624  ringccoALTV  43687