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

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

Proof of Theorem elxp6
StepHypRef Expression
1 elxp4 7860 . 2 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
2 1stval 7924 . . . . 5 (1st𝐴) = dom {𝐴}
3 2ndval 7925 . . . . 5 (2nd𝐴) = ran {𝐴}
42, 3opeq12i 4836 . . . 4 ⟨(1st𝐴), (2nd𝐴)⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩
54eqeq2i 2750 . . 3 (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩)
62eleq1i 2829 . . . 4 ((1st𝐴) ∈ 𝐵 dom {𝐴} ∈ 𝐵)
73eleq1i 2829 . . . 4 ((2nd𝐴) ∈ 𝐶 ran {𝐴} ∈ 𝐶)
86, 7anbi12i 628 . . 3 (((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))
95, 8anbi12i 628 . 2 ((𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
101, 9bitr4i 278 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩ ∧ ((1st𝐴) ∈ 𝐵 ∧ (2nd𝐴) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wcel 2107  {csn 4587  cop 4593   cuni 4866   × cxp 5632  dom cdm 5634  ran crn 5635  cfv 6497  1st c1st 7920  2nd c2nd 7921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-1st 7922  df-2nd 7923
This theorem is referenced by:  elxp7  7957  eqopi  7958  1st2nd2  7961  eldju2ndl  9861  eldju2ndr  9862  r0weon  9949  qredeu  16535  qnumdencl  16615  setsstruct2  17047  tx1cn  22963  tx2cn  22964  txhaus  23001  psmetxrge0  23669  xppreima  31565  ofpreima2  31585  smatrcl  32380  1stmbfm  32863  2ndmbfm  32864  oddpwdcv  32958  prproropf1olem0  45701
  Copyright terms: Public domain W3C validator