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

Theorem elvv 5748
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 5698 . 2 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2 vex 3478 . . . . 5 𝑥 ∈ V
3 vex 3478 . . . . 5 𝑦 ∈ V
42, 3pm3.2i 471 . . . 4 (𝑥 ∈ V ∧ 𝑦 ∈ V)
54biantru 530 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
652exbii 1851 . 2 (∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
71, 6bitr4i 277 1 (𝐴 ∈ (V × V) ↔ ∃𝑥𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3474  cop 4633   × cxp 5673
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210  df-xp 5681
This theorem is referenced by:  elvvv  5749  elvvuni  5750  elopaelxpOLD  5764  elrel  5796  copsex2gb  5804  relop  5848  elreldm  5932  dmsnn0  6203  funsndifnop  7145  1stval2  7988  2ndval2  7989  1st2val  7999  2nd2val  8000  dfopab2  8034  dfoprab3s  8035  dftpos4  8226  tpostpos  8227  fundmen  9027  cnvfi  9176  fundmge2nop0  14449  ssrelf  31831  fineqvac  34085  dfdm5  34732  dfrn5  34733  brtxp2  34841  pprodss4v  34844  brpprod3a  34846  brimg  34897  brxrn2  37233  fun2dmnopgexmpl  45978
  Copyright terms: Public domain W3C validator