Theorem elxp6 7965

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7862. (Contributed by NM, 9-Oct-2004.)

Assertion

Ref	Expression
elxp6	⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))

Proof of Theorem elxp6

Step	Hyp	Ref	Expression
1		elxp4 7862	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
2		1stval 7933	. . . . 5 ⊢ (1st ‘𝐴) = ∪ dom {𝐴}
3		2ndval 7934	. . . . 5 ⊢ (2nd ‘𝐴) = ∪ ran {𝐴}
4	2, 3	opeq12i 4832	. . . 4 ⊢ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩
5	4	eqeq2i 2747	. . 3 ⊢ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ↔ 𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩)
6	2	eleq1i 2825	. . . 4 ⊢ ((1st ‘𝐴) ∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵)
7	3	eleq1i 2825	. . . 4 ⊢ ((2nd ‘𝐴) ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶)
8	6, 7	anbi12i 628	. . 3 ⊢ (((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))
9	5, 8	anbi12i 628	. 2 ⊢ ((𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
10	1, 9	bitr4i 278	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {csn 4578  ⟨cop 4584  ∪ cuni 4861   × cxp 5620  dom cdm 5622  ran crn 5623  ‘cfv 6490  1^st c1st 7929  2^nd c2nd 7930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7931  df-2nd 7932

This theorem is referenced by:  elxp7  7966  eqopi  7967  1st2nd2  7970  eldju2ndl  9834  eldju2ndr  9835  r0weon  9920  qredeu  16583  qnumdencl  16664  setsstruct2  17099  tx1cn  23551  tx2cn  23552  txhaus  23589  psmetxrge0  24255  xppreima  32672  ofpreima2  32693  smatrcl  33902  1stmbfm  34366  2ndmbfm  34367  oddpwdcv  34461  prproropf1olem0  47690