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

Theorem elrnmpt2 6938
Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
rngop.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
elrnmpt2.1 𝐶 ∈ V
Assertion
Ref Expression
elrnmpt2 (𝐷 ∈ ran 𝐹 ↔ ∃𝑥𝐴𝑦𝐵 𝐷 = 𝐶)
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝐷
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem elrnmpt2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 rngop.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
21rnmpt2 6935 . . 3 ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = 𝐶}
32eleq2i 2831 . 2 (𝐷 ∈ ran 𝐹𝐷 ∈ {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = 𝐶})
4 elrnmpt2.1 . . . . . 6 𝐶 ∈ V
5 eleq1 2827 . . . . . 6 (𝐷 = 𝐶 → (𝐷 ∈ V ↔ 𝐶 ∈ V))
64, 5mpbiri 248 . . . . 5 (𝐷 = 𝐶𝐷 ∈ V)
76rexlimivw 3167 . . . 4 (∃𝑦𝐵 𝐷 = 𝐶𝐷 ∈ V)
87rexlimivw 3167 . . 3 (∃𝑥𝐴𝑦𝐵 𝐷 = 𝐶𝐷 ∈ V)
9 eqeq1 2764 . . . 4 (𝑧 = 𝐷 → (𝑧 = 𝐶𝐷 = 𝐶))
1092rexbidv 3195 . . 3 (𝑧 = 𝐷 → (∃𝑥𝐴𝑦𝐵 𝑧 = 𝐶 ↔ ∃𝑥𝐴𝑦𝐵 𝐷 = 𝐶))
118, 10elab3 3498 . 2 (𝐷 ∈ {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = 𝐶} ↔ ∃𝑥𝐴𝑦𝐵 𝐷 = 𝐶)
123, 11bitri 264 1 (𝐷 ∈ ran 𝐹 ↔ ∃𝑥𝐴𝑦𝐵 𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1632  wcel 2139  {cab 2746  wrex 3051  Vcvv 3340  ran crn 5267  cmpt2 6815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277  df-oprab 6817  df-mpt2 6818
This theorem is referenced by:  qexALT  11996  lsmelvalx  18255  efgtlen  18339  frgpnabllem1  18476  fmucndlem  22296  mbfimaopnlem  23621  tglnunirn  25642  tpr2rico  30267  mbfmco2  30636  br2base  30640  dya2icobrsiga  30647  dya2iocnrect  30652  dya2iocucvr  30655  sxbrsigalem2  30657  cntotbnd  33908  eldiophb  37822  elicores  40263  volicorescl  41273
  Copyright terms: Public domain W3C validator