Theorem dmopab 5907

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

Step	Hyp	Ref	Expression
1		nfopab1 5182	. . 3 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2		nfopab2 5183	. . 3 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	1, 2	dfdmf 5888	. 2 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦}
4		df-br 5111	. . . . 5 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5		opabidw 5510	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
6	4, 5	bitri 278	. . . 4 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ 𝜑)
7	6	exbii 1878	. . 3 ⊢ (∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ∃𝑦𝜑)
8	7	abbii 2830	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦} = {𝑥 ∣ ∃𝑦𝜑}
9	3, 8	eqtri 2786	1 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑥 ∣ ∃𝑦𝜑}

Syntax hints:   = wceq 1570  ∃wex 1809   ∈ wcel 2143  {cab 2741  ⟨cop 4596   class class class wbr 5110  {copab 5174  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-dm 5673

This theorem is referenced by:  dmopabelb  5908  dmopabss  5910  dmopab3  5911  mptfnf  6672  opabiotadm  6964  fndmin  7042  dmoprab  7515  zfrep6OLD  7953  hartogslem1  9505  dmttrcl  9691  rankf  9767  dfac3  10106  axdc2lem  10433  shftdm  15110  dfiso2  17830  adjeu  32219  satfdm  35839  fmla0  35852  fmlasuc0  35854