xpopth - Metamath Proof Explorer

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

Theorem xpopth 7167

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.)

**Assertion**
Ref	Expression
xpopth	⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1^st ‘𝐴) = (1^st ‘𝐵) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) ↔ 𝐴 = 𝐵))

**Proof of Theorem xpopth**
Step	Hyp	Ref	Expression
1		1st2nd2 7165	. . 3 ⊢ (𝐴 ∈ (𝐶 × 𝐷) → 𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩)
2		1st2nd2 7165	. . 3 ⊢ (𝐵 ∈ (𝑅 × 𝑆) → 𝐵 = ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩)
3	1, 2	eqeqan12d 2637	. 2 ⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (𝐴 = 𝐵 ↔ ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ = ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩))
4		fvex 6168	. . 3 ⊢ (1^st ‘𝐴) ∈ V
5		fvex 6168	. . 3 ⊢ (2^nd ‘𝐴) ∈ V
6	4, 5	opth 4915	. 2 ⊢ (⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ = ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ↔ ((1^st ‘𝐴) = (1^st ‘𝐵) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)))
7	3, 6	syl6rbb 277	1 ⊢ ((𝐴 ∈ (𝐶 × 𝐷) ∧ 𝐵 ∈ (𝑅 × 𝑆)) → (((1^st ‘𝐴) = (1^st ‘𝐵) ∧ (2^nd ‘𝐴) = (2^nd ‘𝐵)) ↔ 𝐴 = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ⟨cop 4161 × cxp 5082 ‘cfv 5857 1^st c1st 7126 2^nd c2nd 7127

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-sep 4751 ax-nul 4759 ax-pow 4813 ax-pr 4877 ax-un 6914

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ral 2913 df-rex 2914 df-rab 2917 df-v 3192 df-sbc 3423 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-nul 3898 df-if 4065 df-sn 4156 df-pr 4158 df-op 4162 df-uni 4410 df-br 4624 df-opab 4684 df-mpt 4685 df-id 4999 df-xp 5090 df-rel 5091 df-cnv 5092 df-co 5093 df-dm 5094 df-rn 5095 df-iota 5820 df-fun 5859 df-fv 5865 df-1st 7128 df-2nd 7129

This theorem is referenced by: fseqdom 8809 iundom2g 9322 mdetunilem9 20366 txhaus 21390 fsumvma 24872 wlkeq 26433 disjxpin 29287 poimirlem4 33084 poimirlem13 33093 poimirlem14 33094 poimirlem22 33102 poimirlem26 33106 poimirlem27 33107 rmxypairf1o 36995