Theorem elvv 5752

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 5701	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
2		vex 3465	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3465	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	pm3.2i 469	. . . 4 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
5	4	biantru 528	. . 3 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
6	5	2exbii 1843	. 2 ⊢ (∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
7	1, 6	bitr4i 277	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3461  ⟨cop 4636   × cxp 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5212  df-xp 5684

This theorem is referenced by:  elvvv  5753  elvvuni  5754  elopaelxpOLD  5768  elrel  5800  copsex2gb  5808  relop  5853  elreldm  5937  dmsnn0  6213  funsndifnop  7160  1stval2  8011  2ndval2  8012  1st2val  8022  2nd2val  8023  dfopab2  8057  dfoprab3s  8058  dftpos4  8251  tpostpos  8252  fundmen  9056  cnvfi  9205  fundmge2nop0  14489  ssrelf  32484  fineqvac  34848  dfdm5  35499  dfrn5  35500  brtxp2  35608  pprodss4v  35611  brpprod3a  35613  brimg  35664  brxrn2  37977  fun2dmnopgexmpl  46802