Theorem elvv 5722

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 5670	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2		vex 3458	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	pm3.2i 474	. . . 4 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
5	4	biantru 537	. . 3 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
6	5	2exbii 1869	. 2 ⊢ (∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
7	1, 6	bitr4i 280	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1560  ∃wex 1799   ∈ wcel 2142  Vcvv 3454  ⟨cop 4588   × cxp 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-un 3909  df-in 3911  df-ss 3921  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-xp 5653

This theorem is referenced by:  elvvv  5723  elvvuni  5724  elrel  5770  copsex2gb  5779  relop  5822  elreldm  5911  dmsnn0  6194  funsndifnop  7134  1stval2  7987  2ndval2  7988  1st2val  7998  2nd2val  7999  dfopab2  8033  dfoprab3s  8034  dftpos4  8225  tpostpos  8226  fundmen  9012  cnvfi  9144  fundmge2nop0  14515  ssrelf  32814  fineqvac  35409  dfdm5  36120  dfrn5  36121  brtxp2  36226  pprodss4v  36229  brpprod3a  36231  brimg  36282  brxrn2  38880  fun2dmnopgexmpl  47875