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

Theorem elrnmpt1 5282
Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
rnmpt.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
elrnmpt1 ((𝑥𝐴𝐵𝑉) → 𝐵 ∈ ran 𝐹)

Proof of Theorem elrnmpt1
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3175 . . . 4 𝑥 ∈ V
2 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
3 csbeq1a 3507 . . . . . . 7 (𝑥 = 𝑧𝐴 = 𝑧 / 𝑥𝐴)
42, 3eleq12d 2681 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝑧 / 𝑥𝐴))
5 csbeq1a 3507 . . . . . . 7 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
65biantrud 526 . . . . . 6 (𝑥 = 𝑧 → (𝑧𝑧 / 𝑥𝐴 ↔ (𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
74, 6bitr2d 267 . . . . 5 (𝑥 = 𝑧 → ((𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵) ↔ 𝑥𝐴))
87equcoms 1933 . . . 4 (𝑧 = 𝑥 → ((𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵) ↔ 𝑥𝐴))
91, 8spcev 3272 . . 3 (𝑥𝐴 → ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵))
10 df-rex 2901 . . . . . 6 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥𝐴𝑦 = 𝐵))
11 nfv 1829 . . . . . . 7 𝑧(𝑥𝐴𝑦 = 𝐵)
12 nfcsb1v 3514 . . . . . . . . 9 𝑥𝑧 / 𝑥𝐴
1312nfcri 2744 . . . . . . . 8 𝑥 𝑧𝑧 / 𝑥𝐴
14 nfcsb1v 3514 . . . . . . . . 9 𝑥𝑧 / 𝑥𝐵
1514nfeq2 2765 . . . . . . . 8 𝑥 𝑦 = 𝑧 / 𝑥𝐵
1613, 15nfan 1815 . . . . . . 7 𝑥(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵)
175eqeq2d 2619 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦 = 𝐵𝑦 = 𝑧 / 𝑥𝐵))
184, 17anbi12d 742 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵)))
1911, 16, 18cbvex 2259 . . . . . 6 (∃𝑥(𝑥𝐴𝑦 = 𝐵) ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵))
2010, 19bitri 262 . . . . 5 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵))
21 eqeq1 2613 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 = 𝑧 / 𝑥𝐵𝐵 = 𝑧 / 𝑥𝐵))
2221anbi2d 735 . . . . . 6 (𝑦 = 𝐵 → ((𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵) ↔ (𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
2322exbidv 1836 . . . . 5 (𝑦 = 𝐵 → (∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵) ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
2420, 23syl5bb 270 . . . 4 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
25 rnmpt.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
2625rnmpt 5279 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
2724, 26elab2g 3321 . . 3 (𝐵𝑉 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
289, 27syl5ibr 234 . 2 (𝐵𝑉 → (𝑥𝐴𝐵 ∈ ran 𝐹))
2928impcom 444 1 ((𝑥𝐴𝐵𝑉) → 𝐵 ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wex 1694  wcel 1976  wrex 2896  csb 3498  cmpt 4637  ran crn 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-mpt 4639  df-cnv 5036  df-dm 5038  df-rn 5039
This theorem is referenced by:  fliftel1  6438  minveclem4  22956  minvecolem4  26954  rexunirn  28549  esum2d  29316  totbndbnd  32582  rrnequiv  32628  suprnmpt  38174  disjf1o  38197  disjinfi  38199  choicefi  38211  fourierdlem31  38855  ioorrnopnlem  39024  sge0f1o  39099  sge0supre  39106  sge0gerp  39112  sge0iunmpt  39135  sge0rernmpt  39139  sge0reuz  39164  meadjiunlem  39182  iunhoiioolem  39390  vonioolem1  39395
  Copyright terms: Public domain W3C validator