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

Theorem elvv 5711
Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elvv (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem elvv
StepHypRef Expression
1 elxp 5661 . 2 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2 vex 3452 . . . . 5 𝑥 ∈ V
3 vex 3452 . . . . 5 𝑦 ∈ V
42, 3pm3.2i 472 . . . 4 (𝑥 ∈ V ∧ 𝑦 ∈ V)
54biantru 531 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
652exbii 1852 . 2 (∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
71, 6bitr4i 278 1 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  Vcvv 3448  cop 4597   × cxp 5636
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-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
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-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644
This theorem is referenced by:  elvvv  5712  elvvuni  5713  elopaelxpOLD  5727  elrel  5759  copsex2gb  5767  relop  5811  elreldm  5895  dmsnn0  6164  funsndifnop  7102  1stval2  7943  2ndval2  7944  1st2val  7954  2nd2val  7955  dfopab2  7989  dfoprab3s  7990  dftpos4  8181  tpostpos  8182  fundmen  8982  cnvfi  9131  fundmge2nop0  14398  ssrelf  31576  fineqvac  33738  dfdm5  34386  dfrn5  34387  brtxp2  34495  pprodss4v  34498  brpprod3a  34500  brimg  34551  brxrn2  36866  fun2dmnopgexmpl  45590
  Copyright terms: Public domain W3C validator