Theorem elvv 5733

Description: Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.) (Proof shortened by BJ, 16-Oct-2026.)

Assertion

Ref	Expression
elvv	⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem elvv

Step	Hyp	Ref	Expression
1		elxp2 5682	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 ∈ V ∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩)
2		rexv 3481	. 2 ⊢ (∃𝑥 ∈ V ∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩)
3		rexv 3481	. . 3 ⊢ (∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
4	3	exbii 1881	. 2 ⊢ (∃𝑥∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
5	1, 2, 4	3bitri 300	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090  Vcvv 3454  ⟨cop 4840   × cxp 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-op 4841  df-opab 5174  df-xp 5664

This theorem is used by:  elvvv  5735  elvvuni  5736  elrel  5783  copsex2gb  5793  relop  5838  elreldm  5929  dmsnn0  6227  funsndifnop  7187  1stval2  8052  2ndval2  8053  1st2val  8063  2nd2val  8064  dfopab2  8098  dfoprab3s  8099  dftpos4  8300  tpostpos  8301  fundmen  9097  cnvfi  9229  fundmge2nop0  14688  ssrelf  33307  fineqvac  35925  dfdm5  36752  dfrn5  36753  brtxp2  36858  pprodss4v  36861  brpprod3a  36863  brimg  36914  brxrn2  39582  fun2dmnopgexmpl  48627