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

Theorem elrnmpt1 5957
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 3478 . . . 4 𝑥 ∈ V
2 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
3 csbeq1a 3907 . . . . . . 7 (𝑥 = 𝑧𝐴 = 𝑧 / 𝑥𝐴)
42, 3eleq12d 2827 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝑧 / 𝑥𝐴))
5 csbeq1a 3907 . . . . . . 7 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
65biantrud 532 . . . . . 6 (𝑥 = 𝑧 → (𝑧𝑧 / 𝑥𝐴 ↔ (𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
74, 6bitr2d 279 . . . . 5 (𝑥 = 𝑧 → ((𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵) ↔ 𝑥𝐴))
87equcoms 2023 . . . 4 (𝑧 = 𝑥 → ((𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵) ↔ 𝑥𝐴))
91, 8spcev 3596 . . 3 (𝑥𝐴 → ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵))
10 df-rex 3071 . . . . . 6 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥𝐴𝑦 = 𝐵))
11 nfv 1917 . . . . . . 7 𝑧(𝑥𝐴𝑦 = 𝐵)
12 nfcsb1v 3918 . . . . . . . . 9 𝑥𝑧 / 𝑥𝐴
1312nfcri 2890 . . . . . . . 8 𝑥 𝑧𝑧 / 𝑥𝐴
14 nfcsb1v 3918 . . . . . . . . 9 𝑥𝑧 / 𝑥𝐵
1514nfeq2 2920 . . . . . . . 8 𝑥 𝑦 = 𝑧 / 𝑥𝐵
1613, 15nfan 1902 . . . . . . 7 𝑥(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵)
175eqeq2d 2743 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦 = 𝐵𝑦 = 𝑧 / 𝑥𝐵))
184, 17anbi12d 631 . . . . . . 7 (𝑥 = 𝑧 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵)))
1911, 16, 18cbvexv1 2338 . . . . . 6 (∃𝑥(𝑥𝐴𝑦 = 𝐵) ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵))
2010, 19bitri 274 . . . . 5 (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵))
21 eqeq1 2736 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 = 𝑧 / 𝑥𝐵𝐵 = 𝑧 / 𝑥𝐵))
2221anbi2d 629 . . . . . 6 (𝑦 = 𝐵 → ((𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵) ↔ (𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
2322exbidv 1924 . . . . 5 (𝑦 = 𝐵 → (∃𝑧(𝑧𝑧 / 𝑥𝐴𝑦 = 𝑧 / 𝑥𝐵) ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
2420, 23bitrid 282 . . . 4 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
25 rnmpt.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
2625rnmpt 5954 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
2724, 26elab2g 3670 . . 3 (𝐵𝑉 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑧(𝑧𝑧 / 𝑥𝐴𝐵 = 𝑧 / 𝑥𝐵)))
289, 27imbitrrid 245 . 2 (𝐵𝑉 → (𝑥𝐴𝐵 ∈ ran 𝐹))
2928impcom 408 1 ((𝑥𝐴𝐵𝑉) → 𝐵 ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wrex 3070  csb 3893  cmpt 5231  ran crn 5677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5684  df-dm 5686  df-rn 5687
This theorem is referenced by:  fliftel1  7309  minveclem4  24956  minvecolem4  30171  rexunirn  31770  esum2d  33160  exrecfnlem  36346  totbndbnd  36743  rrnequiv  36789  suprnmpt  43952  disjf1o  43969  disjinfi  43970  choicefi  43978  elrnmpt1d  44011  suprubrnmpt  44036  supxrleubrnmpt  44195  suprleubrnmpt  44211  infrnmptle  44212  infxrunb3rnmpt  44217  supminfrnmpt  44234  infxrgelbrnmpt  44243  fourierdlem31  44933  ioorrnopnlem  45099  sge0f1o  45177  sge0supre  45184  sge0gerp  45190  sge0iunmpt  45213  sge0rernmpt  45217  sge0reuz  45242  meadjiunlem  45260  iunhoiioolem  45470  vonioolem1  45475  smfpimcclem  45602
  Copyright terms: Public domain W3C validator