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

Theorem elvv 5603
 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 5555 . 2 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2 vex 3472 . . . . 5 𝑥 ∈ V
3 vex 3472 . . . . 5 𝑦 ∈ V
42, 3pm3.2i 474 . . . 4 (𝑥 ∈ V ∧ 𝑦 ∈ V)
54biantru 533 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
652exbii 1850 . 2 (∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
71, 6bitr4i 281 1 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2114  Vcvv 3469  ⟨cop 4545   × cxp 5530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-opab 5105  df-xp 5538 This theorem is referenced by:  elvvv  5604  elvvuni  5605  elopaelxp  5618  elrel  5648  copsex2gb  5656  relop  5698  elreldm  5782  dmsnn0  6042  funsndifnop  6895  1stval2  7692  2ndval2  7693  1st2val  7703  2nd2val  7704  dfopab2  7736  dfoprab3s  7737  dftpos4  7898  tpostpos  7899  fundmen  8570  fundmge2nop0  13846  ssrelf  30374  dfdm5  33090  dfrn5  33091  brtxp2  33416  pprodss4v  33419  brpprod3a  33421  brimg  33472  brxrn2  35745  fun2dmnopgexmpl  43779
 Copyright terms: Public domain W3C validator