Theorem op1stg 7331

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 4540	. . . 4 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
2	1	fveq2d 6337	. . 3 ⊢ (𝑥 = 𝐴 → (1st ‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝐴, 𝑦⟩))
3		id 22	. . 3 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
4	2, 3	eqeq12d 2786	. 2 ⊢ (𝑥 = 𝐴 → ((1st ‘⟨𝑥, 𝑦⟩) = 𝑥 ↔ (1st ‘⟨𝐴, 𝑦⟩) = 𝐴))
5		opeq2 4541	. . . 4 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
6	5	fveq2d 6337	. . 3 ⊢ (𝑦 = 𝐵 → (1st ‘⟨𝐴, 𝑦⟩) = (1st ‘⟨𝐴, 𝐵⟩))
7	6	eqeq1d 2773	. 2 ⊢ (𝑦 = 𝐵 → ((1st ‘⟨𝐴, 𝑦⟩) = 𝐴 ↔ (1st ‘⟨𝐴, 𝐵⟩) = 𝐴))
8		vex 3354	. . 3 ⊢ 𝑥 ∈ V
9		vex 3354	. . 3 ⊢ 𝑦 ∈ V
10	8, 9	op1st 7327	. 2 ⊢ (1st ‘⟨𝑥, 𝑦⟩) = 𝑥
11	4, 7, 10	vtocl2g 3421	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1st ‘⟨𝐴, 𝐵⟩) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ⟨cop 4323  ‘cfv 6030  1^st c1st 7317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-iota 5993  df-fun 6032  df-fv 6038  df-1st 7319

This theorem is referenced by:  ot1stg  7333  ot2ndg  7334  br1steqg  7341  1stconst  7420  mpt2sn  7423  curry2  7427  mpt2xopn0yelv  7495  mpt2xopoveq  7501  xpmapenlem  8287  1stinl  8957  1stinr  8959  fpwwe  9674  addpipq  9965  mulpipq  9968  ordpipq  9970  swrdval  13625  ruclem1  15166  qnumdenbi  15659  setsstruct  16105  oppccofval  16583  funcf2  16735  cofuval2  16754  resfval2  16760  resf1st  16761  isnat  16814  fucco  16829  homadm  16897  setcco  16940  estrcco  16977  xpcco  17031  xpchom2  17034  xpcco2  17035  evlf2  17066  curfval  17071  curf1cl  17076  uncf1  17084  uncf2  17085  diag11  17091  diag12  17092  diag2  17093  hof2fval  17103  yonedalem21  17121  yonedalem22  17126  mvmulfval  20566  imasdsf1olem  22398  ovolicc1  23504  ioombl1lem3  23548  ioombl1lem4  23549  brcgr  26001  opvtxfv  26105  fgreu  29811  fvtransport  32476  bj-elid3  33423  bj-inftyexpiinv  33431  bj-finsumval0  33483  poimirlem17  33758  poimirlem24  33765  poimirlem27  33768  rngoablo2  34038  dvhopvadd  36901  dvhopvsca  36910  dvhopaddN  36922  dvhopspN  36923  etransclem44  41007  ovnsubaddlem1  41299  ovnlecvr2  41339  ovolval5lem2  41382  rngccoALTV  42511  ringccoALTV  42574