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 8021

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7919. (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 8020	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∧ ((1^st ‘𝐴) ∈ 𝐵 ∧ (2^nd ‘𝐴) ∈ 𝐶)))
2		fvex 6891	. . . . 5 ⊢ (1^st ‘𝐴) ∈ V
3		fvex 6891	. . . . 5 ⊢ (2^nd ‘𝐴) ∈ V
4	2, 3	pm3.2i 476	. . . 4 ⊢ ((1^st ‘𝐴) ∈ V ∧ (2^nd ‘𝐴) ∈ V)
5		elxp6 8020	. . . 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 1570 ∈ wcel 2145 Vcvv 3450 ⟨cop 4590 × cxp 5653 ‘cfv 6533 1^st c1st 7984 2^nd c2nd 7985

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pr 5398 ax-un 7736

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 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-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-iota 6489 df-fun 6535 df-fv 6541 df-1st 7986 df-2nd 7987

This theorem is used by: xp2 8023 unielxp 8024 1stconst 8097 2ndconst 8098 fparlem1 8109 fparlem2 8110 infxpenlem 10016 1stpreimas 33178 1stpreima 33179 2ndpreima 33180 f1od2 33190 xpinpreima2 34417 tpr2rico 34422 sxbrsigalem0 34782 dya2iocnrect 34792 elxp8 38125 pellex 43676 elpglem3 50639

W3C validator