![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > xp1st | GIF version |
Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
xp1st | ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxp 4421 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = 〈𝑏, 𝑐〉 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))) | |
2 | vex 2617 | . . . . . . 7 ⊢ 𝑏 ∈ V | |
3 | vex 2617 | . . . . . . 7 ⊢ 𝑐 ∈ V | |
4 | 2, 3 | op1std 5857 | . . . . . 6 ⊢ (𝐴 = 〈𝑏, 𝑐〉 → (1st ‘𝐴) = 𝑏) |
5 | 4 | eleq1d 2153 | . . . . 5 ⊢ (𝐴 = 〈𝑏, 𝑐〉 → ((1st ‘𝐴) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵)) |
6 | 5 | biimpar 291 | . . . 4 ⊢ ((𝐴 = 〈𝑏, 𝑐〉 ∧ 𝑏 ∈ 𝐵) → (1st ‘𝐴) ∈ 𝐵) |
7 | 6 | adantrr 463 | . . 3 ⊢ ((𝐴 = 〈𝑏, 𝑐〉 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵) |
8 | 7 | exlimivv 1821 | . 2 ⊢ (∃𝑏∃𝑐(𝐴 = 〈𝑏, 𝑐〉 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (1st ‘𝐴) ∈ 𝐵) |
9 | 1, 8 | sylbi 119 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (1st ‘𝐴) ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = wceq 1287 ∃wex 1424 ∈ wcel 1436 〈cop 3428 × cxp 4402 ‘cfv 4972 1st c1st 5847 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-sep 3925 ax-pow 3977 ax-pr 4003 ax-un 4227 |
This theorem depends on definitions: df-bi 115 df-3an 924 df-tru 1290 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ral 2360 df-rex 2361 df-v 2616 df-sbc 2829 df-un 2990 df-in 2992 df-ss 2999 df-pw 3411 df-sn 3431 df-pr 3432 df-op 3434 df-uni 3631 df-br 3815 df-opab 3869 df-mpt 3870 df-id 4087 df-xp 4410 df-rel 4411 df-cnv 4412 df-co 4413 df-dm 4414 df-rn 4415 df-iota 4937 df-fun 4974 df-fv 4980 df-1st 5849 |
This theorem is referenced by: xpf1o 6493 xpmapenlem 6498 djuf1olem 6666 djur 6678 eldju1st 6683 dfplpq2 6834 dfmpq2 6835 enqbreq2 6837 enqdc1 6842 mulpipq2 6851 preqlu 6952 elnp1st2nd 6956 cauappcvgprlemladd 7138 elreal2 7289 cnref1o 9042 frecuzrdgrrn 9718 frec2uzrdg 9719 frecuzrdgrcl 9720 frecuzrdgsuc 9724 frecuzrdgrclt 9725 frecuzrdgg 9726 frecuzrdgsuctlem 9733 iseqvalt 9765 eucalgval 10830 eucalginv 10832 eucalglt 10833 eucialg 10835 sqpweven 10947 2sqpwodd 10948 |
Copyright terms: Public domain | W3C validator |