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

Theorem rnopab 5906
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
StepHypRef Expression
1 nfopab1 5174 . . 3 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 nfopab2 5175 . . 3 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
31, 2dfrnf 5902 . 2 ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦}
4 df-br 5105 . . . . 5 (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opabidw 5479 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
64, 5bitri 275 . . . 4 (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦𝜑)
76exbii 1851 . . 3 (∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ ∃𝑥𝜑)
87abbii 2808 . 2 {𝑦 ∣ ∃𝑥 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦} = {𝑦 ∣ ∃𝑥𝜑}
93, 8eqtri 2766 1 ran {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑦 ∣ ∃𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wex 1782  wcel 2107  {cab 2715  cop 4591   class class class wbr 5104  {copab 5166  ran crn 5632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-cnv 5639  df-dm 5641  df-rn 5642
This theorem is referenced by:  rnmpt  5907  mptpreima  6187  rnoprab  7453  pwfir  9054  marypha2lem4  9308  hartogslem1  9412  rnttrcl  9592  axdc2lem  10318  abrexdomjm  31237  abrexexd  31239  lsmsnorb  31972  satfrnmapom  33744  rnmptsn  35737  abrexdom  36120  rncnvepres  36695  imaopab  40585
  Copyright terms: Public domain W3C validator