Theorem op1stg 7998

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 4840	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6886	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 23	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2785	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4841	. . 3 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveqeq2d 6890	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
7		vex 3465	. . 3 ⊢ 𝑥 ∈ V
8		vex 3465	. . 3 ⊢ 𝑦 ∈ V
9	7, 8	op1st 7994	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
10	4, 6, 9	vtocl2g 3545	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ⟨cop 4598  ‘cfv 6537  1^st c1st 7984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-iota 6493  df-fun 6539  df-fv 6545  df-1st 7986

This theorem is referenced by:  ot1stg  8000  ot2ndg  8001  br1steqg  8008  1stconst  8095  mposn  8098  curry2  8102  opco1  8118  mpoxopn0yelv  8209  mpoxopoveq  8215  xpmapenlem  9132  1stinl  9913  1stinr  9915  fpwwe  10631  addpipq  10922  mulpipq  10925  ordpipq  10927  swrdval  14681  ruclem1  16287  qnumdenbi  16803  setsstruct  17236  oppccofval  17772  funcf2  17925  cofuval2  17944  resfval2  17950  resf1st  17951  isnat  18007  fucco  18022  homadm  18097  setcco  18140  estrcco  18186  xpcco  18239  xpchom2  18242  xpcco2  18243  evlf2  18274  curfval  18279  curf1cl  18284  uncf1  18292  uncf2  18293  diag11  18299  diag12  18300  diag2  18301  hof2fval  18311  yonedalem21  18329  yonedalem22  18334  mvmulfval  22668  imasdsf1olem  24499  ovolicc1  25644  ioombl1lem3  25688  ioombl1lem4  25689  addsqnreup  27573  addsval  28121  mulsval  28268  brcgr  29191  opvtxfv  29295  fgreu  32957  fsuppcurry2  33011  erlbrd  33524  erld2  33527  rlocaddval  33530  rlocmulval  33531  fracerl  33570  sategoelfvb  35844  prv1n  35856  fvtransport  36457  bj-inftyexpiinv  37775  bj-finsumval0  37852  poimirlem17  38211  poimirlem24  38218  poimirlem27  38221  rngoablo2  38483  dvhopvadd  41792  dvhopvsca  41801  dvhopaddN  41813  dvhopspN  41814  etransclem44  46919  ovnsubaddlem1  47211  ovnlecvr2  47251  ovolval5lem2  47294  gpgedgiov  48754  gpgedg2ov  48755  gpgedg2iv  48756  rngccoALTV  48960  ringccoALTV  48994  func1st  49775  oppf1st2nd  49829  upfval3  49876  swapf1val  49965  fucofval  50017  fuco111  50028  fuco21  50034  fucoid  50046  precofval3  50069  prcofvala  50075  prcofval  50076  lanfval  50311  ranfval  50312