op1std - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > op1std		Structured version Visualization version GIF version

Theorem op1std 8009

Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)

**Hypotheses**
Ref	Expression
op1st.1	⊢ 𝐴 ∈ V
op1st.2	⊢ 𝐵 ∈ V

**Assertion**
Ref	Expression
op1std	⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1^st ‘𝐶) = 𝐴)

**Proof of Theorem op1std**
Step	Hyp	Ref	Expression
1		fveq2 6902	. 2 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1^st ‘𝐶) = (1^st ‘⟨𝐴, 𝐵⟩))
2		op1st.1	. . 3 ⊢ 𝐴 ∈ V
3		op1st.2	. . 3 ⊢ 𝐵 ∈ V
4	2, 3	op1st 8007	. 2 ⊢ (1^st ‘⟨𝐴, 𝐵⟩) = 𝐴
5	1, 4	eqtrdi 2784	1 ⊢ (𝐶 = ⟨𝐴, 𝐵⟩ → (1^st ‘𝐶) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 Vcvv 3473 ⟨cop 4638 ‘cfv 6553 1^st c1st 7997

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-opab 5215 df-mpt 5236 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-iota 6505 df-fun 6555 df-fv 6561 df-1st 7999

This theorem is referenced by: 1st2val 8027 xp1st 8031 sbcopeq1a 8059 csbopeq1a 8060 eloprabi 8073 mpomptsx 8074 dmmpossx 8076 fmpox 8077 ovmptss 8104 fmpoco 8106 df1st2 8109 fsplit 8128 frxp 8137 xporderlem 8138 fnwelem 8142 fimaproj 8146 xpord2lem 8153 naddcllem 8703 xpf1o 9170 mapunen 9177 xpwdomg 9616 hsmexlem2 10458 fsumcom2 15760 fprodcom2 15968 qredeu 16636 isfuncd 17858 cofucl 17881 funcres2b 17890 funcpropd 17896 xpcco1st 18182 xpccatid 18186 1stf1 18190 2ndf1 18193 1stfcl 18195 prf1 18198 prfcl 18201 prf1st 18202 prf2nd 18203 evlf1 18219 evlfcl 18221 curf1fval 18223 curf11 18225 curf1cl 18227 curfcl 18231 hof1fval 18252 txbas 23491 cnmpt1st 23592 txhmeo 23727 ptuncnv 23731 ptunhmeo 23732 xpstopnlem1 23733 xkohmeo 23739 prdstmdd 24048 ucnimalem 24205 fmucndlem 24216 fsum2cn 24809 ovoliunlem1 25451 lgsquadlem1 27333 lgsquadlem2 27334 2sqreuop 27415 2sqreuopnn 27416 2sqreuoplt 27417 2sqreuopltb 27418 2sqreuopnnlt 27419 2sqreuopnnltb 27420 clwlkclwwlkfolem 29837 wlkl0 30197 gsumhashmul 32791 eulerpartlemgs2 34033 hgt750lemb 34321 cvmliftlem15 34941 satfv1 35006 satfdmlem 35011 fmlasuc 35029 msubty 35170 msubco 35174 msubvrs 35203 filnetlem4 35898 finixpnum 37111 poimirlem4 37130 poimirlem15 37141 poimirlem20 37146 poimirlem26 37152 poimirlem28 37154 heicant 37161 dicelvalN 40683 aks6d1c2p1 41621 aks6d1c3 41626 aks6d1c4 41627 aks6d1c6lem2 41675 aks6d1c6lem4 41677 aks6d1c7lem1 41684 fmpocos 41756 rmxypairf1o 42363 unxpwdom3 42550 fgraphxp 42663 elcnvlem 43062 dvnprodlem2 45364 etransclem46 45697 ovnsubaddlem1 45987 dmmpossx2 47478 2arymaptf 47803 rrx2plordisom 47874 funcf2lem 48102

W3C validator

	
		OSZAR »