Theorem elvv 5726

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 5675	. 2 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 ∈ V ∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩)
2		rexv 3477	. 2 ⊢ (∃𝑥 ∈ V ∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩)
3		rexv 3477	. . 3 ⊢ (∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
4	3	exbii 1880	. 2 ⊢ (∃𝑥∃𝑦 ∈ V 𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)
5	1, 2, 4	3bitri 300	1 ⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝐴 = ⟨𝑥, 𝑦⟩)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086  Vcvv 3450  ⟨cop 4834   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-un 4150  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-xp 5657

This theorem is used by:  elvvv  5728  elvvuni  5729  elrel  5775  copsex2gb  5785  relop  5829  elreldm  5918  dmsnn0  6211  funsndifnop  7160  1stval2  8022  2ndval2  8023  1st2val  8033  2nd2val  8034  dfopab2  8067  dfoprab3s  8068  dftpos4  8269  tpostpos  8270  fundmen  9066  cnvfi  9198  fundmge2nop0  14654  ssrelf  33260  fineqvac  35844  dfdm5  36633  dfrn5  36634  brtxp2  36739  pprodss4v  36742  brpprod3a  36744  brimg  36795  brxrn2  39425  fun2dmnopgexmpl  48462