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 8040

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7938. (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 8039	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))
2		fvex 6903	. . . . 5 ⊢ (1^st ‘𝐴) ∈ V
3		fvex 6903	. . . . 5 ⊢ (2^nd ‘𝐴) ∈ V
4	2, 3	pm3.2i 476	. . . 4 ⊢ ((1^st ‘𝐴) ∈ V ∧ (2^nd ‘𝐴) ∈ V)
5		elxp6 8039	. . . 4 ⊢ (𝐴 ∈ (V × V) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ V ∧ (2^nd ‘𝐴) ∈ V)))
6	4, 5	mpbiran2 723	. . 3 ⊢ (𝐴 ∈ (V × V) ↔ 𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩)
7	6	anbi1i 636	. 2 ⊢ ((𝐴 ∈ (V × V) ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))
8	1, 7	bitr4i 281	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 ∈ (V × V) ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⟨cop 4834 × cxp 5649 ‘cfv 6543 1^st c1st 8003 2^nd c2nd 8004

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5391 ax-un 7755

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6497 df-fun 6545 df-fv 6551 df-1st 8005 df-2nd 8006

This theorem is used by: xp2 8042 unielxp 8043 f1od2 8114 1stconst 8117 2ndconst 8118 fparlem1 8129 fparlem2 8130 infxpenlem 10099 1stpreimas 33350 1stpreima 33351 2ndpreima 33352 xpinpreima2 34589 tpr2rico 34594 sxbrsigalem0 34953 dya2iocnrect 34963 elxp8 38403 pellex 43951 elpglem3 50989

W3C validator