MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmopab Structured version   Visualization version   GIF version

Theorem dmopab 5926
Description: The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)
Assertion
Ref Expression
dmopab dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem dmopab
StepHypRef Expression
1 nfopab1 5213 . . 3 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 nfopab2 5214 . . 3 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
31, 2dfdmf 5907 . 2 dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦}
4 df-br 5144 . . . . 5 (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opabidw 5529 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
64, 5bitri 275 . . . 4 (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦𝜑)
76exbii 1848 . . 3 (∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ∃𝑦𝜑)
87abbii 2809 . 2 {𝑥 ∣ ∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦} = {𝑥 ∣ ∃𝑦𝜑}
93, 8eqtri 2765 1 dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wex 1779  wcel 2108  {cab 2714  cop 4632   class class class wbr 5143  {copab 5205  dom cdm 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-dm 5695
This theorem is referenced by:  dmopabelb  5927  dmopabss  5929  dmopab3  5930  mptfnf  6703  opabiotadm  6990  fndmin  7065  dmoprab  7536  zfrep6  7979  hartogslem1  9582  dmttrcl  9761  rankf  9834  dfac3  10161  axdc2lem  10488  shftdm  15110  dfiso2  17816  adjeu  31908  satfdm  35374  fmla0  35387  fmlasuc0  35389
  Copyright terms: Public domain W3C validator