Theorem rnopab 5903

Description: The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)

Assertion

Ref	Expression
rnopab	⊢ ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem rnopab

Step	Hyp	Ref	Expression
1		nfopab1 5168	. . 3 ⊢ Ⅎ𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2		nfopab2 5169	. . 3 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	1, 2	dfrnf 5899	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦}
4		df-br 5099	. . . . 5 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5		opabidw 5472	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
6	4, 5	bitri 275	. . . 4 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ 𝜑)
7	6	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ∃𝑥𝜑)
8	7	abbii 2803	. 2 ⊢ {𝑦 ∣ ∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦} = {𝑦 ∣ ∃𝑥𝜑}
9	3, 8	eqtri 2759	1 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑}

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2714  ⟨cop 4586   class class class wbr 5098  {copab 5160  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rnopabss  5904  rnopab3  5905  rnmpt  5906  mptpreima  6196  rnoprab  7463  pwfir  9217  marypha2lem4  9341  hartogslem1  9447  rnttrcl  9631  axdc2lem  10358  abrexdomjm  32582  abrexexd  32584  lsmsnorb  33472  satfrnmapom  35564  rnmptsn  37536  abrexdom  37927  rncnvepres  38498  dfsuccl2  38640  imaopab  42483  tfsconcatrn  43580  modelaxreplem3  45217