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 4809	. . . 4 ⊢ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩
5	4	eqeq2i 2752	. . 3 ⊢ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ↔ 𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩)
6	2	eleq1i 2830	. . . 4 ⊢ ((1st ‘𝐴) ∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵)
7	3	eleq1i 2830	. . . 4 ⊢ ((2nd ‘𝐴) ∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶)
8	6, 7	anbi12i 634	. . 3 ⊢ (((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))
9	5, 8	anbi12i 634	. 2 ⊢ ((𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
10	1, 9	bitr4i 279	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶)))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4555  ⟨cop 4561  ∪ cuni 4838   × cxp 5616  dom cdm 5618  ran crn 5619  ‘cfv 6485  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fv 6493  df-1st 7931  df-2nd 7932

This theorem is referenced by:  elxp7  7966  eqopi  7967  1st2nd2  7970  eldju2ndl  9839  eldju2ndr  9840  r0weon  9925  qredeu  16618  qnumdencl  16700  setsstruct2  17135  tx1cn  23592  tx2cn  23593  txhaus  23630  psmetxrge0  24296  xppreima  32737  ofpreima2  32758  smatrcl  33980  1stmbfm  34444  2ndmbfm  34445  oddpwdcv  34539  prproropf1olem0  47977