Theorem elvv 5693

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

Step	Hyp	Ref	Expression
1		elxp 5641	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2		vex 3435	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3435	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	pm3.2i 471	. . . 4 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
5	4	biantru 534	. . 3 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
6	5	2exbii 1856	. 2 ⊢ (∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
7	1, 6	bitr4i 279	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431  ⟨cop 4561   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-in 3890  df-ss 3900  df-sn 4556  df-pr 4558  df-op 4562  df-opab 5135  df-xp 5624

This theorem is referenced by:  elvvv  5694  elvvuni  5695  elrel  5741  copsex2gb  5749  relop  5792  elreldm  5877  dmsnn0  6158  funsndifnop  7094  1stval2  7948  2ndval2  7949  1st2val  7959  2nd2val  7960  dfopab2  7994  dfoprab3s  7995  dftpos4  8185  tpostpos  8186  fundmen  8968  cnvfi  9100  fundmge2nop0  14455  ssrelf  32707  fineqvac  35297  dfdm5  36001  dfrn5  36002  brtxp2  36107  pprodss4v  36110  brpprod3a  36112  brimg  36163  brxrn2  38751  fun2dmnopgexmpl  47747