Theorem elvv 5726

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 5674	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2		vex 3455	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3455	. . . . 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 3451  ⟨cop 4590   × cxp 5649

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5657

This theorem is used by:  elvvv  5727  elvvuni  5728  elrel  5774  copsex2gb  5784  relop  5828  elreldm  5917  dmsnn0  6207  funsndifnop  7153  1stval2  8016  2ndval2  8017  1st2val  8027  2nd2val  8028  dfopab2  8061  dfoprab3s  8062  dftpos4  8255  tpostpos  8256  fundmen  9052  cnvfi  9184  fundmge2nop0  14640  ssrelf  33202  fineqvac  35767  dfdm5  36517  dfrn5  36518  brtxp2  36623  pprodss4v  36626  brpprod3a  36628  brimg  36679  brxrn2  39296  fun2dmnopgexmpl  48323