Theorem xp1st 6281

Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
xp1st	⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Proof of Theorem xp1st

Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 4713	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 2782	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 2782	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op1std 6264	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (1st ‘𝐴) = 𝑏)
5	4	eleq1d 2278	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵))
6	5	biimpar 297	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵)
7	6	adantrr 479	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
8	7	exlimivv 1923	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵)
9	1, 8	sylbi 121	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1375  ∃wex 1518   ∈ wcel 2180  ⟨cop 3649   × cxp 4694  ‘cfv 5294  1^st c1st 6254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-iota 5254  df-fun 5296  df-fv 5302  df-1st 6256

This theorem is referenced by:  disjxp1  6352  xpf1o  6973  xpmapenlem  6978  opabfi  7068  djuf1olem  7188  eldju1st  7206  exmidapne  7414  dfplpq2  7509  dfmpq2  7510  enqbreq2  7512  enqdc1  7517  mulpipq2  7526  preqlu  7627  elnp1st2nd  7631  cauappcvgprlemladd  7813  elreal2  7985  cnref1o  9814  frecuzrdgrrn  10597  frec2uzrdg  10598  frecuzrdgrcl  10599  frecuzrdgsuc  10603  frecuzrdgrclt  10604  frecuzrdgg  10605  frecuzrdgsuctlem  10612  seq3val  10649  seqvalcd  10650  fsum2dlemstep  11911  fisumcom2  11915  fprod2dlemstep  12099  fprodcom2fi  12103  eucalgval  12542  eucalginv  12544  eucalglt  12545  eucalg  12547  sqpweven  12663  2sqpwodd  12664  ctiunctlemudc  12974  xpsff1o  13348  tx2cn  14909  txdis  14916  txhmeo  14958  xmetxp  15146  xmetxpbl  15147  xmettxlem  15148  xmettx  15149  lgsquadlemofi  15720  lgsquadlem1  15721  lgsquadlem2  15722