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

Theorem elxp6 7534
Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7441. (Contributed by NM, 9-Oct-2004.)
Assertion
Ref Expression
elxp6 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)))

Proof of Theorem elxp6
StepHypRef Expression
1 elxp4 7441 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
2 1stval 7502 . . . . 5 (1st𝐴) = dom {𝐴}
3 2ndval 7503 . . . . 5 (2nd𝐴) = ran {𝐴}
42, 3opeq12i 4679 . . . 4 ⟨(1st𝐴), (2nd𝐴)⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩
54eqeq2i 2785 . . 3 (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩)
62eleq1i 2851 . . . 4 ((1st𝐴) ∈ 𝐵 dom {𝐴} ∈ 𝐵)
73eleq1i 2851 . . . 4 ((2nd𝐴) ∈ 𝐶 ran {𝐴} ∈ 𝐶)
86, 7anbi12i 618 . . 3 (((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))
95, 8anbi12i 618 . 2 ((𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
101, 9bitr4i 270 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 387   = wceq 1508  wcel 2051  {csn 4436  cop 4442   cuni 4709   × cxp 5402  dom cdm 5404  ran crn 5405  cfv 6186  1st c1st 7498  2nd c2nd 7499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-iota 6150  df-fun 6188  df-fv 6194  df-1st 7500  df-2nd 7501
This theorem is referenced by:  elxp7  7535  eqopi  7536  1st2nd2  7539  eldju2ndl  9146  eldju2ndr  9147  r0weon  9231  qredeu  15857  qnumdencl  15934  setsstruct2  16376  tx1cn  21937  tx2cn  21938  txhaus  21975  psmetxrge0  22642  xppreima  30174  ofpreima2  30191  smatrcl  30736  1stmbfm  31196  2ndmbfm  31197  oddpwdcv  31291  prproropf1olem0  43062
  Copyright terms: Public domain W3C validator