elxp7 - Metamath Proof Explorer

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

Theorem elxp7 7866

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7769. (Contributed by NM, 19-Aug-2006.)

**Assertion**
Ref	Expression
elxp7	⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))

**Proof of Theorem elxp7**
Step	Hyp	Ref	Expression
1		elxp6 7865	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))
2		fvex 6787	. . . . 5 ⊢ (1^st ‘𝐴) ∈ V
3		fvex 6787	. . . . 5 ⊢ (2^nd ‘𝐴) ∈ V
4	2, 3	pm3.2i 471	. . . 4 ⊢ ((1^st ‘𝐴) ∈ V ∧ (2^nd ‘𝐴) ∈ V)
5		elxp6 7865	. . . 4 ⊢ (𝐴 ∈ (V × V) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ V ∧ (2^nd ‘𝐴) ∈ V)))
6	4, 5	mpbiran2 707	. . 3 ⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩)
7	6	anbi1i 624	. 2 ⊢ ((𝐴 ∈ (V × V) ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))
8	1, 7	bitr4i 277	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 Vcvv 3432 ⟨cop 4567 × cxp 5587 ‘cfv 6433 1^st c1st 7829 2^nd c2nd 7830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 df-2nd 7832

This theorem is referenced by: xp2 7868 unielxp 7869 1stconst 7940 2ndconst 7941 fparlem1 7952 fparlem2 7953 infxpenlem 9769 1stpreimas 31038 1stpreima 31039 2ndpreima 31040 f1od2 31056 xpinpreima2 31857 tpr2rico 31862 sxbrsigalem0 32238 dya2iocnrect 32248 elxp8 35542 pellex 40657 elpglem3 46418

W3C validator