![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elxp6 | Structured version Visualization version GIF version |
Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7441. (Contributed by NM, 9-Oct-2004.) |
Ref | Expression |
---|---|
elxp6 | ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxp4 7441 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) | |
2 | 1stval 7502 | . . . . 5 ⊢ (1st ‘𝐴) = ∪ dom {𝐴} | |
3 | 2ndval 7503 | . . . . 5 ⊢ (2nd ‘𝐴) = ∪ ran {𝐴} | |
4 | 2, 3 | opeq12i 4679 | . . . 4 ⊢ 〈(1st ‘𝐴), (2nd ‘𝐴)〉 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 |
5 | 4 | eqeq2i 2785 | . . 3 ⊢ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ↔ 𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉) |
6 | 2 | eleq1i 2851 | . . . 4 ⊢ ((1st ‘𝐴) ∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵) |
7 | 3 | eleq1i 2851 | . . . 4 ⊢ ((2nd ‘𝐴) ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶) |
8 | 6, 7 | anbi12i 618 | . . 3 ⊢ (((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)) |
9 | 5, 8 | anbi12i 618 | . 2 ⊢ ((𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
10 | 1, 9 | bitr4i 270 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 = wceq 1508 ∈ wcel 2051 {csn 4436 〈cop 4442 ∪ cuni 4709 × cxp 5402 dom cdm 5404 ran crn 5405 ‘cfv 6186 1st c1st 7498 2nd c2nd 7499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-iota 6150 df-fun 6188 df-fv 6194 df-1st 7500 df-2nd 7501 |
This theorem is referenced by: elxp7 7535 eqopi 7536 1st2nd2 7539 eldju2ndl 9146 eldju2ndr 9147 r0weon 9231 qredeu 15857 qnumdencl 15934 setsstruct2 16376 tx1cn 21937 tx2cn 21938 txhaus 21975 psmetxrge0 22642 xppreima 30174 ofpreima2 30191 smatrcl 30736 1stmbfm 31196 2ndmbfm 31197 oddpwdcv 31291 prproropf1olem0 43062 |
Copyright terms: Public domain | W3C validator |