Theorem elvv 5734

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 5682	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2		vex 3457	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3457	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	pm3.2i 476	. . . 4 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
5	4	biantru 539	. . 3 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
6	5	2exbii 1882	. 2 ⊢ (∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
7	1, 6	bitr4i 281	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3453  ⟨cop 4593   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-un 3907  df-in 3909  df-ss 3919  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-xp 5665

This theorem is used by:  elvvv  5735  elvvuni  5736  elrel  5782  copsex2gb  5791  relop  5834  elreldm  5923  dmsnn0  6207  funsndifnop  7152  1stval2  8007  2ndval2  8008  1st2val  8018  2nd2val  8019  dfopab2  8053  dfoprab3s  8054  dftpos4  8247  tpostpos  8248  fundmen  9042  cnvfi  9174  fundmge2nop0  14571  ssrelf  33096  fineqvac  35650  dfdm5  36360  dfrn5  36361  brtxp2  36466  pprodss4v  36469  brpprod3a  36471  brimg  36522  brxrn2  39140  fun2dmnopgexmpl  48180